proposition: Lemma distn_eq1 n1 n2 : (`|n1 - n2| == 1) = (if n1 < n2 then n1.+1 == n2 else n1 == n2.+1).
proof: Proof. case: ltnP => [lt_n12 | le_n21]. by rewrite eq_sym -(eqn_add2r n1) distnEr ?subnK // ltnW. by rewrite -(eqn_add2r n2) distnEl ?subnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)