Nuprl Lemma : vr_add_ge

a,b:

. (0

(a + b))

Proof not projected

Definitions occuring in Statement : nat:

, le: A

B, all:

x:A. B[x], add: n + m, natural_number: $n
Definitions : tactic: Error :tactic, nat:

, member: t

T, function: x:A

B[x], all:

x:A. B[x], int:

, add: n + m, equal: s = t, natural_number: $n, le: A

B, false: False, implies: P

Q, not:

A, prop:

, less_than: a < b, subtype: S

T, grp_car: |g|, real:

, set: {x:A| B[x]}
Lemmas : nat_wf, false_wf, not_wf

\mforall{}a,b:\mBbbN{}. (0 \mleq{} (a + b)) Date html generated: 2012_02_20-PM-03_31_48 Last ObjectModification: 2012_02_02-PM-01_55_03 Home Index