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.
ntheorem le_O_n : ∀n:nat. O ≤ n.
#n; nelim n; /2/; nqed.
-ntheorem nboh: 0 ≤ 0 + 0.
-//; nqed.
-
ntheorem le_n_Sn : ∀n:nat. n ≤ 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/;