theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.