fact: Definition add_divisors f divs := let: (p, e) := f in let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in iter e add1 divs.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)