proposition: Lemma eqR_le x y : (x = y) <-> (x <= y <= x).
proof: Proof. split => [->| [] ]; by [split; exact/Rle_refl | exact: Rle_antisym]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)