proposition: Lemma mul_min_distr_r n m p : min (n * p) (m * p) = min n m * p.
proof: Proof. rewrite 3 (mul_comm _ p). apply mul_min_distr_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef