proposition: Lemma leq_up_log p m n : m <= n -> up_log p m <= up_log p n.
proof: Proof. move=> mLn; case: p => [|[|p]] //. by apply/up_log_min => //; apply: leq_trans mLn (up_logP _ _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)