proposition: Theorem mk_lelt_inf: forall l H, ~In inf_elt (mk_lelt l H).
proof: Proof. intros l; elim l; simpl; auto. intros (x, y) l1 Hrec H H1; simpl. inversion_clear H1; try discriminate. case (Hrec (fun (x1 y1 : K) (Hxy1 : In (x1, y1) l1) => H x1 y1 (or_intror ((x, y) = (x1, y1)) Hxy1))); auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith