proposition: Lemma leq_logn_trunc p m k : (1 < p)%N -> (m <= k)%N -> (logn p m <= trunc_log p k)%N.
proof: Proof. case: m => [|m]; rewrite ?logn0 //. move=> h1p leq_mk; apply: trunc_log_max=> //; apply: leq_trans leq_mk. by rewrite -p_part dvdn_leq // dvdn_part. Qed.
imports: mathcomp(all_ssreflect all_algebra)