fact: Fixpoint sg_tab n : seq (seq int) := if n is m.+1 then flatten (map (fun x => map (fun l => x :: l) (sg_tab m)) [::1; -1; 0]) else [::[::]].
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)