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