]
qed.
+lemma arith_l3 (m) (n1) (n2): n1+n2-m = n1-m+(n2-(m-n1)).
+// qed.
+
lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
-* // qed.
+#n1 #n2 <arith_l3 //
+qed.
lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
-// qed.
+#x <arith_l2 //
+qed.
+
+lemma arith_m2 (x) (y): x < y → x+(y-↑x) = ↓y.
+#x #y #Hxy >minus_minus [|*: // ] <minus_Sn_n //
+qed-.