proposition: Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.
proof: Proof. elim/ltn_ind: m n => -[|m] IHm [|n] //=; rewrite /gcdn -/gcdn. case def_p: (_ %% _) => // [p]. have{def_p} lt_pm: p.+1 < m.+1 by rewrite -def_p ltn_pmod. rewrite {}IHm // subn_if_gt ltnW //=; congr gcdn. by rewrite -(subnK (ltnW lt_pm)) modnDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)