proposition: Lemma rmin_prop1 x y (r := rmin x y): realp x -> realp y -> [/\ realp r, r <=r x & r <=r y].
proof: Proof. move => sa sb; rewrite / r/ rmin; Ytac h; split => //;try BRo_tac. case: (rleT_ee sa sb) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)