+theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to
+ \exists s. r = (S s) \land add p q s.
+ intros. inversion H; clear H; intros;
+ [ lapply eq_gen_S_O to H as H0. apply H0
+ | lapply eq_gen_S_S to H2 as H0. clear H2.
+ rewrite > H0. clear H0.
+ apply ex_intro; [| auto ] (**)
+ ].
+qed.
+