proposition: Lemma distnDr d n1 n2 : `|n1 + d - (n2 + d)| = `|n1 - n2|.
proof: Proof. by rewrite -!(addnC d) distnDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)