- \forall q2,r2. (r1 + q2 == r2) \to
- \exists q. (q1 + q2 == q) \land p + q == r2.
+ \forall q2,r2. (r1 + q2 == r2) \to
+ \exists q. (q1 + q2 == q) \land p + q == r2.
- \forall p2,r2. (p2 + r1 == r2) \to
- \exists p. (p1 + p2 == p) \land p + q == r2.
+ \forall p2,r2. (p2 + r1 == r2) \to
+ \exists p. (p1 + p2 == p) \land p + q == r2.
intros 2; elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
rewrite > H0. clear H0 p1
intros 2; elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
rewrite > H0. clear H0 p1
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
rewrite > H0 in H1. clear H0 p
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
rewrite > H0 in H1. clear H0 p