fact: Fixpoint logn_rec d m r := match r, edivn m d with | r'.+1, (_.+1 as m', 0) => (logn_rec d m' r').+1 | _, _ => 0 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)