proposition: Lemma dvdn_gcdr m n : gcdn m n %| n.
proof: Proof. elim/ltn_ind: m n => -[|m] IHm [|n] //=. rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p. have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod. rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; last exact: IHm. by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)