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 //
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 //