proposition: Lemma distnEr n1 n2 : n1 <= n2 -> `|n1 - n2| = n2 - n1.
proof: Proof. by move/subnK=> {1}<-; rewrite distnC PoszD addrK absz_nat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)