proposition: Lemma pnat_1 pi n : pi.-nat n -> pi^'.-nat n -> n = 1.
proof: Proof. by move=> pi_n pi'_n; rewrite -(eqnP (pnat_coprime pi_n pi'_n)) gcdnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)