fact: Fixpoint EKa (l: list K) : list (K * K) := match l with | nil => nil | x :: l1 => let y := kplus (kplus (x ^ 3) (kmul A x)) B in match KLroot y with | Some k => if k ?0 then (x, kO) :: EKa l1 else (x, k) :: (x, kopp k) :: EKa l1 | None => EKa l1 end end.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith