proposition: Theorem mk_lelt_length: forall l H, length (mk_lelt l H) = length l.
proof: Proof. intros l; elim l; simpl; auto. intros (x, y) l1 Hrec H; simpl; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith