a b : a * S b =N= a + a * b. Proof. induction a as [| a IHa]. - reflexivity. - change (S (b + a * S b) = S (a + (b + a * b))). apply (ap S). rhs rapply add_assoc. rhs rapply (ap (fun x => x + _) (add_comm _ _)). rhs rapply (add_assoc _ _ _)^. exact (ap (plus b) IHa). Qed.
Require Import