From: Andrea Asperti Date: Tue, 23 Mar 2010 15:52:29 +0000 (+0000) Subject: Re-proved an axiom X-Git-Tag: make_still_working~2980 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0a5e353bdadc4194e8becc7b960088ed4dbf68c1;p=helm.git Re-proved an axiom From: asperti --- diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index 54ff253c2..4f1f65411 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -(* include "higher_order_defs/functions.ma". *) include "hints_declaration.ma". include "basics/functions.ma". include "basics/eq.ma". @@ -80,7 +79,11 @@ ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m). napply nat_elim2; #n; ##[ ncases n; /2/; ##| /3/; - ##| #m; #Hind; ncases Hind; /3/; + ##| #m; #Hind; ncases Hind;/3/; + (* + ##[/2/; ##|#H; nwhd; + napply or_introl; + napply eq_f2; /3/; *) ##] nqed. @@ -450,7 +453,9 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m → (* le and eq *) ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m. -napply nat_elim2; /4/; nqed. +napply nat_elim2; +##[#n; #H1; #H2; /4/; + nqed. ntheorem lt_O_S : ∀n:nat. O < S n. /2/; nqed. @@ -886,7 +891,7 @@ ntheorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m. ntheorem plus_minus_m_m: ∀n,m:nat. m ≤ n → n = (n-m)+m. -#n; #m; #lemn; napplyS symmetric_eq; +#n; #m; #lemn; napplyS sym_eq; napplyS (plus_minus m n m); //; nqed. ntheorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m. @@ -905,7 +910,7 @@ nqed. ntheorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p. (* /4/ done in 43.5 *) #n; #m; #p; #eqp; -napply symmetric_eq; +napply sym_eq; napplyS (minus_plus_m_m p m); nqed. @@ -1045,15 +1050,14 @@ simplify.unfold Not.intro.apply H1.apply inj_S.assumption. qed. *) -naxiom eqb_elim : ∀ n,m:nat.∀ P:bool → Prop. +ntheorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop. (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). -(* napply nat_elim2; ##[#n; ncases n; nnormalize; /3/; ##|nnormalize; /3/; ##|nnormalize; /4/; ##] -nqed.*) +nqed. ntheorem eqb_n_n: ∀n. eqb n n = true. #n; nelim n; nnormalize; //.