proposition: Lemma Rmin_max : forall x y, Rmin (Rmin x y) (Rmax x y) = Rmin x y.
proof: Proof. intros x y. apply Rmin_left. apply Rle_trans with x. apply Rmin_l. apply Rmax_l. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)