lemma pred_S: ∀m. pred (S m) = m.
// qed.
+lemma plus_S1: ∀x,y. ⫯(x+y) = (⫯x) + y.
+// qed.
+
lemma max_O1: ∀n. n = (0 ∨ n).
// qed.
(* Equations ****************************************************************)
+lemma plus_SO: ∀n. n + 1 = ⫯n.
+// qed.
+
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
// qed-.
(* Inversion & forward lemmas ***********************************************)
+lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
+/4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
+qed-.
+
+lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
+/2 width=1 by plus_le_0/ qed-.
+
lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
// qed-.
lemma lt_le_false: ∀x,y. x < y → y ≤ x → ⊥.
/3 width=4 by lt_refl_false, lt_to_le_to_lt/ qed-.
+lemma succ_inv_refl_sn: ∀x. ⫯x = x → ⊥.
+#x #H @(lt_le_false x (⫯x)) //
+qed-.
+
lemma lt_inv_O1: ∀n. 0 < n → ∃m. ⫯m = n.
* /2 width=2 by ex_intro/
#H cases (lt_le_false … H) -H //