proposition: Lemma leR_max x y z : max(y, z) <= x <-> (y <= x) /\ (z <= x).
proof: Proof. split => [| [yx zx] ]. move/RleP. rewrite Order.POrderTheory.le_eqVlt => /orP[/eqP <-|/RltP/Rmax_Rlt]. by split; [exact: leR_maxl | exact: leR_maxr]. by case=> ?; split; exact/ltRW. by rewrite -(Rmax_right _ _ yx); exact: Rle_max_compat_l. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)