proposition: Lemma Rmin_l : forall x y, x<=y -> Rmin x y = x.
proof: Proof. unfold Rmin. intros. destruct Rle_dec as [H'|H']; [| apply Rnot_le_lt in H' ]; unfold Rle in *; intuition. Qed.
imports: Orders Rbase Rbasic_fun ROrderedType GenericMinMax