proposition: Lemma dist0 (s t : T) : dist s t = 0 -> s = t.
proof: Proof. move => D0. move : (distP s t). rewrite D0 addn0. rewrite !modn_small ?ltn_ord //. move/ord_inj. move/enum_rank_inj. by symmetry. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)