proposition: Lemma muln_gcdr : right_distributive muln gcdn.
proof: Proof. move=> p m n; have [-> //|p_gt0] := posnP p. elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0). by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)