(* Equations ****************************************************************)
+lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
+// qed-.
+
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
(* Inversion & forward lemmas ***********************************************)
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
/2 width=1 by monotonic_pred/ qed-.
lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
/2 width=4 by plus_xySz_x_false/ qed-.
+(* Note this should go in nat.ma *)
+lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+#x @(nat_ind_plus … x) -x /2 width=1 by or_introl/
+#x #_ #y @(nat_ind_plus … y) -y /2 width=1 by or_intror/
+#y #_ >minus_plus_plus_l
+#H lapply (discr_plus_xy_minus_xz … H) -H
+#H destruct
+qed-.
+
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
(* Iterators ****************************************************************)
(* Note: see also: lib/arithemetics/bigops.ma *)