proposition: Lemma leR_eqVlt m n : (m <= n) <-> (m = n) \/ (m < n).
proof: Proof. split => [|[->|]]; [ |exact: Rle_refl|exact: ltRW]. by case/Rle_lt_or_eq_dec => ?; [right|left]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)