proposition: Lemma partn_gcd pi m n : m > 0 -> n > 0 -> (gcdn m n)`_pi = gcdn m`_pi n`_pi.
proof: Proof. move=> m_gt0 n_gt0; have p_gt0: gcdn m n > 0 by rewrite gcdn_gt0 m_gt0. apply/eqP; rewrite eqn_dvd dvdn_gcd !partn_dvd ?dvdn_gcdl ?dvdn_gcdr //=. rewrite -(dvdn_pmul2r (part_gt0 pi^' (gcdn m n))) partnC // dvdn_gcd. rewrite -[m in _ %| m](partnC pi m_gt0) andbC -[n in _%| n](partnC pi n_gt0). by rewrite !dvdn_mul ?partn_dvd ?dvdn_gcdl ?dvdn_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)