#n #IH <nplus_succ_dx <nminus_succ_bi //
qed.
-(*** minus_plus_m_m *)
+(*** minus_plus_m_m_commutative *)
lemma nminus_plus_sn_refl_dx (m) (n): m = n + m - n.
#m #n <nplus_comm //
qed.
theorem nminus_plus_assoc (o) (m) (n): o-m-n = o-(m+n).
#o #m #n @(nat_ind_succ โฆ n) -n //
#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
-qed-.
+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_comm //
+#m #n #o <nminus_plus_assoc <nminus_comm_21 //
qed.
(* Helper constructions with nplus ******************************************)
| โงโง ๐ = n & ๐ = o.
#m #n @(nat_ind_2_succ โฆ m n) -m -n
[ /3 width=1 by or_introl, conj/
-| #m #o #Ho
+| #m #_ #o #Ho
lapply (eq_inv_nplus_bi_sn โฆ (๐) Ho) -Ho
/3 width=1 by or_intror, conj/
| #m #n #IH #o