proposition: Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R.
proof: Proof. intros x y. apply Rmin_case_strong; intros H. rewrite Rmax_left; trivial. now apply Ropp_le_contravar. rewrite Rmax_right; trivial. now apply Ropp_le_contravar. Qed.
imports: Coq(Psatz Reals ZArith) Zaux