proposition: Lemma Rmin_r : forall x y, y<=x -> Rmin x y = y.
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