proposition: Lemma opp_min_distr : forall n m : R, - (Rmin n m) = Rmax (- n) (- m).
proof: Proof. intros. symmetry. apply max_min_antimonotone. do 3 red. intros; apply Rge_le. apply Ropp_le_ge_contravar; auto. Qed.
imports: Orders Rbase Rbasic_fun ROrderedType GenericMinMax