proposition: Theorem EKa_elt: forall l x y, In (x, y) (EKa l) -> In_curve x y.
proof: Proof. unfold In_curve; intros l x y; elim l; simpl; auto. intros H; case H. intros a l1 Hrec. generalize (KLroot_root (kplus (kplus (kmul a (kmul a a)) (kmul A a)) B)); case KLroot; auto. intros k Hk; generalize (Eth.(is_zero_correct) k); case is_zero; simpl; intros HH HH1; case HH; intros H1 H2; case HH1; intros H3; subst; clear HH HH1; auto. injection H3; intros; subst y x; rewrite <- H1; auto. injection H3; intros; subst; auto. case H3; clear H3; intros H3; auto. injection H3; intros; subst; rewrite <- Hk; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith