proposition: Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n -> {in pi, logn^~ m =1 logn^~ n} -> m`_pi = n`_pi.
proof: Proof. move=> m0 n0 eq_log; rewrite !(@widen_partn (maxn m n)) ?leq_maxl ?leq_maxr//. by apply: eq_bigr => p /eq_log ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)