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