fact: Definition ccount_weak p sq : R := let fix aux s (i : nat) := if i is i'.+1 then aux (taqsR p sq i' * coefs R (size sq) i' + s) i' else s in aux 0 (3 ^ size sq)%N.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)