### Nuprl Lemma : q_le-elim

`∀[r,s:ℚ].  (q_le(r;s) ~ qpositive(s + -(r)) ∨bqeq(r;s))`

Proof

Definitions occuring in Statement :  q_le: `q_le(r;s)` qpositive: `qpositive(r)` qmul: `r * s` qadd: `r + s` rationals: `ℚ` qeq: `qeq(r;s)` bor: `p ∨bq` uall: `∀[x:A]. B[x]` minus: `-n` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` q_le: `q_le(r;s)` uimplies: `b supposing a` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` qsub: `r - s`
Lemmas referenced :  valueall-type-has-valueall rationals_wf rationals-valueall-type evalall-reduce
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination hypothesisEquality callbyvalueReduce because_Cache sqequalAxiom isect_memberEquality

Latex:
\mforall{}[r,s:\mBbbQ{}].    (q\_le(r;s)  \msim{}  qpositive(s  +  -(r))  \mvee{}\msubb{}qeq(r;s))

Date html generated: 2016_05_15-PM-10_40_39
Last ObjectModification: 2015_12_27-PM-07_58_16

Theory : rationals

Home Index