proposition: Lemma distP s t : enum_rank t = enum_rank s + dist s t %[mod #|{:T}|].
proof: Proof. apply/eqP. by case/andP: (xchooseP (ex_dist (enum_rank s) (enum_rank t) Tgt0)). Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)