proposition: Lemma distS (s t : T) n : dist s t = n.+1 -> dist (next s) t = n.
proof: Proof. move => Dn. move: (distP s t) => H. rewrite Dn -addn1 [_ + 1]addnC addnA addn1 -modnDml in H. move: (distP (next s) t) => Dn'. rewrite {1}/next enum_valK /= in Dn'. apply: unique_dist Dn' H; last rewrite -Dn ltnW //; exact: dist_ltn. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)