proposition: Lemma lem1aux : forall l : list B, GoodR B R l -> forall us : list (A * B), l = sndL us -> MinD us -> GBarlR us.
proof: Proof. Proof using declt. intros l; elim l; auto. intros H'; inversion H'. intros a l0 H' H'0; inversion H'0; auto. intros us; elim us; simpl in |- *; auto. intros; discriminate. intros a1 l2 H'1 H'2 H'3; inversion H'2. apply lem0; auto. rewrite <- H2; rewrite <- H3; auto. inversion H'3; auto. intros us; elim us; unfold sndL in |- *; simpl in |- *; auto. intros; discriminate. intros a1 l2 H'1 H'2 H'3; inversion H'2. change (GBarlR (nil ++ (a1 :: nil) ++ l2)) in |- *. red in |- *; apply monGRBar; simpl in |- *; auto. apply H'; auto. inversion H'3; auto. Qed.
imports: Coq(List PeanoNat Wf_nat Inverse_Image) Buchberger(Bar OpenIndGoodRel Monomials)