proposition: Lemma card_finRing_gt1 (R : finRingType) : 1 < #|R|.
proof: Proof. by rewrite (cardD1 0) (cardD1 1) !inE GRing.oner_neq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)