proposition: Lemma size_sg_tab n : size (sg_tab n) = (3 ^ n)%N.
proof: Proof. by elim: n => [|n] // ihn; rewrite !size_cat !size_map ihn addn0 exp3S. Qed.
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)