proposition: Fact le_total : total le.
proof: Proof. move=> x y; rewrite !le_def; have [->|] //= := eqVneq; rewrite -subr_eq0. by move/lt0_total; rewrite -(sub_gt0 (x - y)) sub0r opprB !sub_gt0 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)