proposition: Lemma lem0 : forall (l : list (A * B)) (a : A * B), ExistsL B (fun x : B => R x (snd a)) (sndL l) -> MinD l -> GBarlR (a :: l).
proof: Proof. Proof using declt. intros l; elim l; simpl in |- *; auto. intros a H' H'0; inversion H'. intros a l0 H' a0 H'0 H'1; inversion H'0. simpl in H0; simpl in H1; simpl in H. case (declt (fst a0) (fst a)); intros LtE. change (GBarlR ((a0 :: nil) ++ (a :: nil) ++ l0)) in |- *; auto. red in |- *; apply monGRBar; simpl in |- *; auto. inversion H'1; auto. red in |- *; red in |- *; apply Base. apply FoundG. apply FoundE. unfold ProdRel in |- *; split; auto. change (GBarlR ((a0 :: nil) ++ (a :: nil) ++ l0)) in |- *; auto. red in |- *; apply monGRBar; simpl in |- *; auto. inversion H'1; simpl in |- *; auto. apply H'; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)