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-.