(* *)
(**************************************************************************)
+include "arithmetics/nat.ma".
+include "ground_2/xoa/ex_3_1.ma".
+include "ground_2/xoa/or_3.ma".
include "ground_2/notation/functions/uparrow_1.ma".
include "ground_2/notation/functions/downarrow_1.ma".
-include "arithmetics/nat.ma".
include "ground_2/pull/pull_2.ma".
include "ground_2/lib/relations.ma".
lemma plus_SO_dx (n): n + 1 = ↑n.
// qed.
+lemma minus_SO_dx (n): n-1 = ↓n.
+// qed.
+
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
// qed-.
lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
/2 width=2 by le_plus_minus_comm/ qed-.
-lemma plus2_inv_le_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+lemma plus2_le_sn_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
#m1 #m2 #n1 #n2 #H #Hm
lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
/2 width=2 by le_plus_to_le/
qed-.
+lemma plus2_le_sn_dx: ∀m1,m2,n1,n2. m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_sn: ∀m1,m2,n1,n2. n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
+lemma plus2_le_dx_dx: ∀m1,m2,n1,n2. n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
+/2 width=4 by plus2_le_sn_sn/ qed-.
+
lemma lt_S_S_to_lt: ∀x,y. ↑x < ↑y → x < y.
/2 width=1 by le_S_S_to_le/ qed-.