proposition: Lemma card_elt : (#|(Finite.clone _ (elt A B))| <= #|K|.*2.+1)%N.
proof: Proof. rewrite !cardT. pose ff b x := if Kroot (x ^+ 3 + A * x + B) is Some y then elt_g A B (Some (x , if b then y else - y)) else None. pose l := inf_elt A B :: pmap (ff true) (enum K) ++ pmap (ff false) (enum K). apply: leq_trans (_ : size l <= _)%N; last first. by rewrite /= ltnS size_cat !size_pmap -addnn leq_add // count_size. apply: uniq_leq_size (enum_uniq _) _ => [] [|x y e] iE. by rewrite in_cons eqxx. rewrite in_cons mem_cat. have := Kroot_spec (x ^+ 3 + A * x + B). case E : Kroot => [y1|]; last by move=> /(_ y); rewrite -e eqxx. move=> y1E. have /eqP : (y ^+ 2 = y1 ^+ 2) by rewrite e. rewrite !mem_pmap eqf_sqr => /orP[] /eqP y1E1. suff -> : Some (curve_elt e) = ff true x by rewrite map_f ?orbT ?mem_enum. rewrite /ff E /=; case: eqP => [p|[]//]. by congr (Some _); apply: curve_elt_irr. suff -> : Some (curve_elt e) = ff false x by rewrite map_f ?orbT ?mem_enum. rewrite /ff E /=; case: eqP => [p|[]]; last by rewrite sqrrN. by congr (Some _); apply: curve_elt_irr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)