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.
##[#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/;