ndefinition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
ndefinition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
ntheorem decidable_le: ∀n,m. decidable (n≤m).
napply nat_elim2; #n; /3/;
ntheorem decidable_le: ∀n,m. decidable (n≤m).
napply nat_elim2; #n; /3/;
ntheorem decidable_lt: ∀n,m. decidable (n < m).
#n; #m; napply decidable_le ; nqed.
ntheorem decidable_lt: ∀n,m. decidable (n < m).
#n; #m; napply decidable_le ; nqed.
ntheorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 \to m1 ≤ m2
→ n1 + m1 ≤ n2 + m2.
ntheorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 \to m1 ≤ m2
→ n1 + m1 ≤ n2 + m2.