qed.
theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
intros 1. elim p; clear p;
[ lapply linear nplus_inv_zero_1 to H
| lapply linear nplus_inv_succ_1_3 to H1.
qed.
theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
intros 1. elim p; clear p;
[ lapply linear nplus_inv_zero_1 to H
| lapply linear nplus_inv_succ_1_3 to H1.