ndefinition not_zero: nat → Prop ≝
λn: nat. match n with
[ O ⇒ False | (S p) ⇒ True ].
-
+
ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
-#n; napply nmk; #eqOS; nchange with (not_zero O); nrewrite > eqOS; //.
+#n; napply nmk; #eqOS; nchange with (not_zero O);
+nrewrite > eqOS; //.
nqed.
ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
##[ ncases n; /2/;
##| /3/;
##| #m; #Hind; ncases Hind;/3/;
- (*
- ##[/2/; ##|#H; nwhd;
- napply or_introl;
- napply eq_f2; /3/; *)
##]
nqed.
#n; nelim n; nnormalize; //; nqed.
ntheorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
-//; nqed.
+//; nqed.
ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
#n; nelim n; nnormalize; /3/; nqed.
#n; #m; #lenm; nelim lenm; /2/;nqed.
ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
-(* XXX *) nletin hint ≝ monotonic.
-#a; #b; #H; napplyS monotonic_pred;
/2/; nqed.
(* this are instances of the le versions
(* le and eq *)
ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-napply nat_elim2;
-##[#n; #H1; #H2; /4/;
- nqed.
+napply nat_elim2; /4/;
+nqed.
ntheorem lt_O_S : ∀n:nat. O < S n.
/2/; nqed.
##[#q; #HleO; (* applica male *)
napply (le_n_O_elim ? HleO);
napply H; #p; #ltpO;
- napply False_ind; /2/; (* 3 *)
+ napply (False_ind ??); /2/; (* 3 *)
##|#p; #Hind; #q; #HleS;
napply H; #a; #lta; napply Hind;
napply le_S_S_to_le;/2/;