fact: Definition prime_decomp n := let: (e2, m2) := elogn2 0 n.-1 n.-1 in if m2 < 2 then 2 ^? e2 :: 3 ^? m2 :: [::] else let: (a, bc) := edivn m2.-2 3 in let: (b, c) := edivn (2 - bc) 2 in 2 ^? e2 :: [rec m2.*2.+1, 1, a, b, c, 0].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)