variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O.
intros 2. elim q; clear q; intros;
variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O.
intros 2. elim q; clear q; intros;
theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
intros 2. elim q; clear q; intros;
theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
intros 2. elim q; clear q; intros;
rewrite < H0 in H3. clear H0 a
]; auto.
qed.
theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
intros 1. elim p; clear p; intros;
rewrite < H0 in H3. clear H0 a
]; auto.
qed.
theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
intros 1. elim p; clear p; intros;