proposition: Lemma unique_dist i j n d d' : d < n -> d' < n -> (j = i + d %[mod n]) -> (j = i + d' %[mod n]) -> d = d'.
proof: Proof. move => Hd Hd' -> /eqP. by rewrite eqn_modDl !modn_small // => /eqP. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)