proposition: Lemma mul_succ_l p q : (succ p) * q = q + p * q.
proof: Proof. induction p as [p IHp | p IHp | ]; simpl; trivial. - now rewrite IHp, add_assoc, add_diag, <-add_xO. - symmetry; apply add_diag. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef