proposition: Lemma real_neqr_lt : {in real &, forall x y, (x != y) = (x < y) || (y < x)}.
proof: Proof. by move=> * /=; case: real_ltgtP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)