proposition: Lemma leq_trunc_log p m n : m <= n -> trunc_log p m <= trunc_log p n.
proof: Proof. move=> mlen; case: p => [|[|p]]; rewrite ?trunc_log0n ?trunc_log1n //. case: m mlen => [|m] mlen; first by rewrite trunc_log0. apply/trunc_log_max => //; apply: leq_trans mlen; exact: trunc_logP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)