proposition: Fact le_def' x y : (x <= y) = (`|y - x| == y - x).
proof: Proof. wlog ->: x y / x = 0 by move/(_ 0 (y - x)); rewrite subr0 sub_ge0 => ->. rewrite {x}subr0; apply/idP/eqP=> [/ge0_norm// | Dy]. by have [//| ny_ge0] := leN_total y; rewrite -Dy -normN ge0_norm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)