proposition: Lemma modn_def m d : m %% d = (edivn m d).2.
proof: Proof. case: d => //= d; rewrite /modn /edivn /=; elim/ltn_ind: m 0 => -[|m] IHm q //=. by rewrite !subn_if_gt; case: (d <= m) => //; apply/IHm/leq_subr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)