fact: Definition trunc_log p n := let fix loop n k := if k is k'.+1 then if p <= n then (loop (n %/ p) k').+1 else 0 else 0 in if p <= 1 then 0 else loop n n.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)