proposition: Lemma Rmax_l : forall x y, y<=x -> Rmax x y = x.
proof: Proof. unfold Rmax. 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