proposition: Lemma logn_coprime p m : coprime p m -> logn p m = 0.
proof: Proof. by move=> coprime_pm; rewrite -[m]muln1 logn_Gauss// logn1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)