proposition: Lemma sub_pnat_coprime pi rho m n : {subset rho <= pi^'} -> pi.-nat m -> rho.-nat n -> coprime m n.
proof: Proof. by move=> pi'rho pi_m /(sub_in_pnat (in1W pi'rho)); apply: pnat_coprime. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)