proposition: Lemma Rmin_opp_Rmax : forall a b, Rmin (-a) (-b) = - Rmax a b.
proof: Proof. intros. rewrite Rmax_comm. unfold Rmin ; case Rle_dec ; intro Hab. apply Ropp_le_cancel in Hab. unfold Rmax ; case Rle_dec ; intuition. apply Rnot_le_lt, Ropp_lt_cancel, Rlt_not_le in Hab. unfold Rmax ; case Rle_dec ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)