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