proposition: Lemma Rmin_Rgt_l : forall r1 r2 r, Rmin r1 r2 > r -> r1 > r /\ r2 > r.
proof: Proof. intros r1 r2 r; unfold Rmin; case (Rle_dec r1 r2) as [Hle|Hnle]; intros. - split. + assumption. + unfold Rgt; exact (Rlt_le_trans r r1 r2 H Hle). - split. + generalize (Rnot_le_lt r1 r2 Hnle); intro; exact (Rgt_trans r1 r2 r H0 H). + assumption. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp