proposition: Lemma ex_dist i j n : (0 < n) -> exists d, (d < n) && (j == i + d %[mod n]).
proof: Proof. move => n0. case: (leqP i j) => H. - exists ((j - i) %% n). by rewrite ltn_mod n0 /= modnDmr (subnKC H). - exists ((n - i %% n + j %% n) %% n). rewrite ltn_mod n0 /= modnDmr. rewrite -(eqn_modDr (i %% n)). set i' := i %% n. set j' := j %% n. rewrite -!addnA [j' + _]addnC. rewrite [n - _ +_]addnA subnK. by rewrite addnC modnDml eqn_modDl modnDmr modnDl. by rewrite ltnW // ltn_mod n0. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)