proposition: Lemma Rmax_opp_Rmin : forall a b, Rmax (-a) (-b) = - Rmin a b.
proof: Proof. intros. destruct (Rle_or_lt a b). rewrite Rmax_left. rewrite Rmin_left. reflexivity. apply H. apply Ropp_le_contravar. apply H. rewrite Rmax_right. rewrite Rmin_right. reflexivity. apply Rlt_le, H. apply Ropp_le_contravar. apply Rlt_le. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)