proposition: Lemma minRE x y : min(x, y) = if (x < y)%mcR then x else y.
proof: Proof. by case: ifP => /RltP; [move/ltRW/Rmin_left|rewrite -leRNgt => /Rmin_right]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)