proposition: Lemma mul_max_distr_l n m p : max (p * n) (p * m) = p * max n m.
proof: Proof. apply max_monotone. intros x x'. apply mul_le_mono_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef