Nuprl Lemma : le_to_lt_rw
∀[i,j:ℤ].  {uiff(i ≤ j;i < j + 1)}
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 : 
le_to_lt
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
lemma_by_obid
Latex:
\mforall{}[i,j:\mBbbZ{}].    \{uiff(i  \mleq{}  j;i  <  j  +  1)\}
Date html generated:
2016_05_14-AM-07_20_23
Last ObjectModification:
2015_12_26-PM-01_32_25
Theory : int_2
Home
Index