proposition: Lemma le_total : Order.POrder_isTotal ring_display R.
proof: Proof. constructor=> x y; move: (real (x - y)). by rewrite unfold_in /= !ler_def subr0 add0r opprB orbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)