proposition: Theorem FELLK_length: (length FELLK <= 2 * length LK + 1)%nat.
proof: Proof. unfold FELLK; rewrite Nat.add_comm; simpl. rewrite mk_lelt_length. generalize ELK_length; simpl; auto with arith. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith