(*** plus_plus_comm_23 *)
lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
#o #m #n >nplus_assoc >nplus_assoc <nplus_comm in โข (??(??%)?); //
(*** plus_plus_comm_23 *)
lemma nplus_plus_comm_23 (o) (m) (n): o + m + n = o + n + m.
#o #m #n >nplus_assoc >nplus_assoc <nplus_comm in โข (??(??%)?); //
lemma eq_inv_zero_nplus (m) (n): ๐ = m + n โ โงโง ๐ = m & ๐ = n.
#m #n @(nat_ind_succ โฆ n) -n
[ /2 width=1 by conj/
lemma eq_inv_zero_nplus (m) (n): ๐ = m + n โ โงโง ๐ = m & ๐ = n.
#m #n @(nat_ind_succ โฆ n) -n
[ /2 width=1 by conj/
(*** injective_plus_l *)
lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o โ m = n.
#o @(nat_ind_succ โฆ o) -o /3 width=1 by eq_inv_nsucc_bi/
(*** injective_plus_l *)
lemma eq_inv_nplus_bi_dx (o) (m) (n): m + o = n + o โ m = n.
#o @(nat_ind_succ โฆ o) -o /3 width=1 by eq_inv_nsucc_bi/