proposition: Lemma ltR_neqAle m n : (m < n) <-> (m <> n) /\ (m <= n).
proof: Proof. split. by move=> /RltP; rewrite Order.POrderTheory.lt_neqAle => /andP[/eqP ? /RleP]. move=> [/eqP mn /RleP nm]. by apply/RltP; rewrite Order.POrderTheory.lt_neqAle mn. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)