proposition: Theorem mul_assoc p q r : p * (q * r) = p * q * r.
proof: Proof. induction p as [p IHp| p IHp | ]; simpl; rewrite ?IHp; trivial. now rewrite mul_add_distr_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef