proposition: Lemma up_log_min p k j : 1 < p -> k <= p ^ j -> up_log p k <= j.
proof: Proof. case: k => [|[|k]] // p_gt1 kLj; rewrite ?(up_log0, up_log1) //. rewrite -[up_log _ _]prednK ?up_log_gt0 ?p_gt1 // -(@ltn_exp2l p) //. by apply: leq_trans (up_log_gtn p_gt1 (isT : 1 < k.+2)) _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)