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