proposition: Lemma Rminmax : forall a b, Rmin a b <= Rmax a b.
proof: Proof. intros a b; destruct (Rle_dec a b). - rewrite Rmin_left, Rmax_right; assumption. - now rewrite Rmin_right, Rmax_left; assumption || apply Rlt_le, Rnot_le_gt. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp