proposition: Theorem mul_comm p q : p * q = q * p.
proof: Proof. induction q as [q IHq|q IHq| ]; simpl; rewrite <- ? IHq; auto using mul_xI_r, mul_xO_r, mul_1_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef