proposition: Lemma gcdnAC : right_commutative gcdn.
proof: Proof. suffices dvd m n p: gcdn (gcdn m n) p %| gcdn (gcdn m p) n. by move=> m n p; apply/eqP; rewrite eqn_dvd !dvd. rewrite !dvdn_gcd dvdn_gcdr. by rewrite !(dvdn_trans (dvdn_gcdl _ p)) ?dvdn_gcdl ?dvdn_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)