proposition: Theorem EKa_complete: forall l x y, In x l -> In_curve x y -> In (x, y) (EKa l).
proof: Proof. unfold In_curve; intros l x y; elim l; simpl; auto. intros a l1 Hrec [H1 | H1] H2; subst; auto. generalize (KLroot_root (kplus (kplus (kmul x (kmul x x)) (kmul A x)) B)); case KLroot; auto. intros k Hk; rewrite <- Hk in H2. case (@Kmult_integral (kplus y k) (ksub y k)); try intros H3. apply trans_equal with (ksub (kmul y y) (kmul k k)); try ring. rewrite H2; ring. generalize (Eth.(is_zero_correct) k); case is_zero; intros HH; case HH; intros H4 H5; clear HH. rewrite <- H3; rewrite H4; auto; simpl; left. apply f_equal2 with (f := @pair K K); auto; ring. right; left; apply f_equal2 with (f := @pair K K); auto. apply trans_equal with (ksub (kplus y k) k); try ring; rewrite H3; ring. generalize (Eth.(is_zero_correct) k); case is_zero; intros HH; case HH; intros H4 H5; clear HH. rewrite <- H3; rewrite H4; auto; simpl; left. apply f_equal2 with (f := @pair K K); auto; ring. left; apply f_equal2 with (f := @pair K K); auto. apply trans_equal with (kplus (ksub y k) k); try ring; rewrite H3; ring. intros H3; case (H3 y); auto. case KLroot; auto. intros k; case is_zero; repeat right; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith