proposition: Theorem EKa_length: forall l, (length (EKa l) <= 2 * length l)%nat.
proof: Proof. intros l; elim l; simpl; auto. intros a l1 H; case KLroot. intros k; case is_zero; simpl. apply le_n_S. apply Nat.le_trans with (1 := H). rewrite <- plus_n_Sm; auto. rewrite <- plus_n_Sm; auto with arith. apply Nat.le_trans with (1 := H). rewrite <- plus_n_Sm; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith