proposition: Lemma mul_max_distr_nonpos_l n m p : p <= 0 -> max (p * n) (p * m) == p * min n m.
proof: Proof. intros. destruct (le_ge_cases n m). - rewrite min_l by trivial. rewrite max_l by now apply mul_le_mono_nonpos_l. reflexivity. - rewrite min_r by trivial. rewrite max_r by now apply mul_le_mono_nonpos_l. reflexivity. Qed.
imports: ZAxioms ZMulOrder GenericMinMax