λn. match n with [ O ⇒ O | S p ⇒ p].
definition not_zero: nat → Prop ≝
- λn: nat. match n with [ O ⇒ ⊥ | (S p) ⇒ ⊤ ].
+ λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
(* order relations *)
theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n).
/2/ qed.
-theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
-/2/ qed.
-
theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
// qed.
(* Negated equalities *******************************************************)
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
theorem not_eq_O_S : ∀n:nat. 0 ≠ S n.
#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
→ n1 + m1 ≤ n2 + m2.
#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
-/2/ qed-.
+/2/ qed.
theorem le_plus_n :∀n,m:nat. m ≤ n + m.
/2/ qed.
#a #b #c #H @(le_plus_to_le_r … b) /2/
qed.
+lemma lt_to_le: ∀x,y. x < y → x ≤ y.
+/2 width=2/ qed.
+
+lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
+// qed-.
+
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
(* lt *)
theorem transitive_lt: transitive nat lt.
@nat_elim2 #n
[#abs @False_ind /2/
|/2/
- |#m #Hind #HnotleSS @le_S_S /3/
+ |#m #Hind #HnotleSS @le_S_S @Hind /2/
]
qed.
(* not lt, le *)
theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
-/4/ qed.
+#n #m #H @le_S_S_to_le @not_le_to_lt /2/ qed.
theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
#n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
qed.
lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
-/3 width=2/ qed-.
+/3/ qed-.
lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
-/3 width=2/ qed-.
+/3/ qed-.
lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
+#m #n elim (decidable_lt m n) /2/ /3/
qed-.
lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m.
-#m #n elim (decidable_le m n) /2 width=1/ /4 width=2/
+#m #n elim (decidable_le m n) /2/ /4/
qed-.
(* More general conclusion **************************************************)
theorem nat_ind_plus: ∀R:predicate nat.
R 0 → (∀n. R n → R (n + 1)) → ∀n. R n.
-/3 width=1 by nat_ind/ qed-.
+/3 by nat_ind/ qed-.
theorem lt_O_n_elim: ∀n:nat. 0 < n →
∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
]
qed.
+lemma f_ind: ∀A. ∀f:A→ℕ. ∀P:predicate A.
+ (∀n. (∀a. f a < n → P a) → ∀a. f a = n → P a) → ∀a. P a.
+#A #f #P #H #a
+cut (∀n,a. f a = n → P a) /2 width=3/ -a
+#n @(nat_elim1 … n) -n #n /3 width=3/ (**) (* auto very slow (274s) without #n *)
+qed-.
+
(* More negated equalities **************************************************)
theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
#n (cases n) // #a #abs @False_ind /2/ qed.
theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-@nat_elim2 /4/
+@nat_elim2 /4 by le_n_O_to_eq, monotonic_pred, eq_f, sym_eq/
qed.
theorem increasing_to_injective: ∀f:nat → nat.
@(ex_intro ?? (S a)) /2/
qed.
+(* thus is le_plus
lemma le_plus_compatible: ∀x1,x2,y1,y2. x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
-/3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+#x1 #y1 #x2 #y2 #H1 #H2 /2/ @le_plus // /2/ /3 by le_minus_to_plus, monotonic_le_plus_r, transitive_le/ qed.
+*)
+
+lemma minus_le: ∀x,y. x - y ≤ x.
+/2 width=1/ qed.
(* lt *)
theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
-#Heq /3/ qed-.
+#Heq @not_le_to_lt /2/ qed-.
theorem lt_times_n_to_lt_l:
∀n,p,q:nat. p*n < q*n → p < q.
@lt_plus_to_minus_r <plus_minus_m_m //
qed.
+(* More compound conclusion *************************************************)
+
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
(* Still more equalities ****************************************************)
theorem eq_minus_O: ∀n,m:nat.
theorem distributive_times_minus: distributive ? times minus.
#a #b #c
(cases (decidable_lt b c)) #Hbc
- [> eq_minus_O /2/ >eq_minus_O //
+ [> eq_minus_O [2:/2/] >eq_minus_O //
@monotonic_le_times_r /2/
|@sym_eq (applyS plus_to_minus) <distributive_times_plus
@eq_f (applyS plus_minus_m_m) /2/
lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
/2 width=1/ qed.
+lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
+// qed.
+
(* Stilll more atomic conclusion ********************************************)
(* le *)