proposition: Theorem EKa_ulist: forall l, ulist l -> ulist (EKa l).
proof: Proof. intros l; elim l; simpl; auto. intros a l1 Hrec H; inversion_clear H. generalize (KLroot_root (kplus (kplus (kmul a (kmul a a)) (kmul A a)) B)); case KLroot; auto. intros k Hk; case (Eth.(is_zero_correct) k); case is_zero. intros H2 _; constructor; auto. apply EKa_in; auto. intros _ H2; repeat constructor; auto. simpl; intros H3; inversion_clear H3. injection H; intros H3. case (@Kmult_integral (kplus kI kI) k). apply trans_equal with (kplus k (kopp k)); [rewrite H3 |idtac]; ring. intros H4; case two_not_zero; auto. intros H5; assert (H6 := H2 H5); discriminate. case (EKa_in l1 a k); auto. apply EKa_in; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith