(* *)
(**************************************************************************)
-(* include "higher_order_defs/functions.ma". *)
include "hints_declaration.ma".
include "basics/functions.ma".
include "basics/eq.ma".
napply nat_elim2; #n;
##[ ncases n; /2/;
##| /3/;
- ##| #m; #Hind; ncases Hind; /3/;
+ ##| #m; #Hind; ncases Hind;/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.
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.
#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; /4/; nqed.
+napply nat_elim2; /4/;
+nqed.
ntheorem lt_O_S : ∀n:nat. O < S n.
/2/; nqed.
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.
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.
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; //.