#n #IH <nplus_succ_dx <nminus_succ_bi //
qed.
+(*** minus_plus_m_m *)
lemma nminus_plus_sn_refl_dx (m) (n): m = n + m - n.
#m #n <nplus_comm //
qed.
(*** minus_plus_plus_l *)
lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
-#m #n #o <nminus_plus_assoc <nminus_minus_comm //
+#m #n #o <nminus_plus_assoc <nminus_comm //
qed.
-(*** plus_minus_plus_plus_l *) (**)
-lemma plus_minus_plus_plus_l: ∀z,x,y,h. z + (x + h) - (y + h) = z + x - y.
-// qed-.
-
(* Helper constructions with nplus ******************************************)
(*** plus_to_minus *)
m + o = m - n →
∨∨ ∧∧ 𝟎 = m & 𝟎 = o
| ∧∧ 𝟎 = n & 𝟎 = o.
-#m #n @(nat_ind_succ_2 … m n) -m -n
+#m #n @(nat_ind_2_succ … m n) -m -n
[ /3 width=1 by or_introl, conj/
| #m #o #Ho
lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
| #m #n #IH #o
<nminus_succ_bi >nplus_succ_shift #Ho
elim (IH … Ho) -IH -Ho * #_ #H
- elim (eq_inv_nzero_succ … H)
+ elim (eq_inv_zero_nsucc … H)
]
qed-.