proposition: Lemma trivg0 : (@set0 gT == 1) = false.
proof: Proof. by rewrite eqEcard cards0 cards1 andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)