proposition: Lemma mul_succ_r p q : p * (succ q) = p + p * q.
proof: Proof. rewrite mul_comm, mul_succ_l. f_equal. apply mul_comm. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef