proposition: Lemma Rmax_opp_opp_Rmin : forall r1 r2, Rmax (-r1) (-r2) = - (Rmin r1 r2).
proof: Proof. intros r1 r2. replace (Rmin r1 r2) with (Rmin (--r1) (--r2)) by (rewrite Ropp_involutive ; intuition (auto with real)). rewrite Rmin_opp_opp_Rmax ; rewrite Ropp_involutive ; reflexivity. Qed.
imports: RIneq MyNeq Rfunctions Lra