1 include "hints_declaration.ma".
2 include "basics/eq.ma".
4 ninductive nat : Type ≝
8 interpretation "Natural numbers" 'N = nat.
10 alias num (instance 0) = "nnatural number".
14 {n:>nat; is_pos: n ≠ 0}.
16 ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on
19 (* default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind.
23 λn. match n with [ O ⇒ O | S p ⇒ p].
25 ntheorem pred_Sn : ∀n. n = pred (S n).
28 ntheorem injective_S : injective nat nat S.
32 ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
35 ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
38 ndefinition not_zero: nat → Prop ≝
40 [ O ⇒ False | (S p) ⇒ True ].
42 ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
43 #n; napply nmk; #eqOS; nchange with (not_zero O);
47 ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
48 #n; nelim n;/2/; nqed.
52 (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n.
53 #n; #P; nelim n; /2/; nqed.
59 → (∀n,m:nat. R n m → R (S n) (S m))
61 #R; #ROn; #RSO; #RSS; #n; nelim n;//;
62 #n0; #Rn0m; #m; ncases m;/2/; nqed.
64 ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
68 ##| #m; #Hind; ncases Hind;/3/;