proposition: Lemma opp_min_distr n m : -(min n m) == max (-n) (-m).
proof: Proof. destruct (le_ge_cases n m). - rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono. - rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono. Qed.
imports: ZAxioms ZMulOrder GenericMinMax