proposition: Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x).
proof: Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)