proposition: Lemma Rmin_Rle : forall r1 r2 r, (Rmin r1 r2 <= r)%R <-> (r1 <= r)%R \/ (r2 <= r)%R.
proof: Proof. intros. unfold Rmin. split. case (Rle_dec r1 r2) ; intros. left. exact H. right. exact H. intros [H|H] ; case (Rle_dec r1 r2) ; intros H0. exact H. apply Rle_trans with (2 := H). apply Rlt_le. apply Rnot_le_lt with (1 := H0). apply Rle_trans with r2 ; assumption. exact H. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)