proposition: Lemma sg_tab_nil n : (sg_tab n == [::]) = false.
proof: Proof. by elim: n => //= n; case: sg_tab. 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)