proposition: Lemma eq_addl_mul q q' m m' d : m < d -> m' < d -> (q * d + m == q' * d + m')%N = ((q, m) == (q', m')).
proof: Proof. move=> lt_md lt_m'd; apply/eqP/eqP; last by move=> [-> ->]. by move=> /(f_equal (edivn^~ d)); rewrite !edivn_eq. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)