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