Nuprl Lemma : lt_to_le_rw
∀[i,j:ℤ]. {uiff(i < j;(i + 1) ≤ j)}
Proof
Definitions occuring in Statement :
less_than: a < b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
guard: {T},
le: A ≤ B,
add: n + m,
natural_number: $n,
int: ℤ
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
lt_to_le
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}[i,j:\mBbbZ{}]. \{uiff(i < j;(i + 1) \mleq{} j)\}
Date html generated:
2016_05_14-AM-07_20_21
Last ObjectModification:
2015_12_26-PM-01_32_24
Theory : int_2
Home
Index