proposition: Lemma mul_max_distr_nonneg_l n m p : 0 <= p -> max (p * n) (p * m) == p * max n m.
proof: Proof. intros. destruct (le_ge_cases n m); [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l. Qed.
imports: ZAxioms ZMulOrder GenericMinMax