#o #m #n elim n -n //
#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
qed-.
(*** minus_plus_plus_l *)
lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
#o #m #n elim n -n //
#n #IH <nplus_succ_dx <nminus_succ_dx <nminus_succ_dx //
qed-.
(*** minus_plus_plus_l *)
lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).