proposition: Lemma enumE : enum A = a :: b :: [::].
proof: Proof. apply (@eq_from_nth _ a); first by rewrite -cardE A2. case=> [_|]; first by rewrite [X in _ = X]/= {2}/a (enum_val_nth a). case=> [_ |i]; last by rewrite -cardE A2. by rewrite [X in _ = X]/= {1}/b (enum_val_nth a). Qed.
imports: mathcomp(all_ssreflect fingroup perm)