proposition: Theorem ConfluentReduce_imp_Grobner : forall Q : list (poly A0 eqA ltM), ConfluentReduce Q -> Grobner Q.
proof: Proof. Proof using os cs. intros Q H'; elim H'. intros H'0. apply Grobner0; auto. intros p q H'1; generalize q; clear q; elim H'1. intros q H'2. rewrite pO_reducestar with (1 := H'2); auto. intros a p0 q s H'2 H'3 H'4 H'5 H'6 q0 H'7. cut (canonical A0 eqA ltM q); [ intros Op0 | apply inPolySet_imp_canonical with (L := Q) ]; auto. cut (canonical A0 eqA ltM p0); [ intros Op2 | apply CombLinear_canonical with (Q := Q) ]; auto. cut (canonical A0 eqA ltM s); [ intros Op1 | idtac ]. cut (canonical A0 eqA ltM q0); [ intros Op2b | idtac ]; auto. cut (reducestar A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q (mults (A:=A) multA (n:=n) a q) (pO A n)); [ intros H'11 | apply reducestar_in_pO with (1 := cs) ]; auto. elim red_minus_zero_reduce with (1 := cs) (Q := Q) (p := s) (q := p0) (ltM_dec := ltM_dec) (eqA_dec := eqA_dec); auto. intros r1 H; elim H; intros H0 H1; clear H. elim reduce0_reducestar with (ltM_dec := ltM_dec) (eqA_dec := eqA_dec) (1 := cs) (Q := Q) (p := r1); auto. intros t E'. lapply (H'0 s); [ intros H'12; inversion H'12 | idtac ]; auto. apply H; auto. apply reducestar_eqp_com with (1 := cs) (p := s) (q := t); auto. apply reducestar_trans with (y := r1) (1 := cs); auto. apply H'5; auto. apply (reducestar_trans A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os Q) with (y := r1); auto. apply canonical_reduceplus with (1 := cs) (3 := H1); auto. apply reduceplus_eqp_com with (1 := cs) (p := mults (A:=A) multA (n:=n) a q) (q := pO A n); auto. inversion H'11; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0) p0); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p0)); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p0 (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p0))); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) (pO A n)); auto. inversion H'7. apply canonical_reduceplus with (1 := cs) (3 := H); auto. apply eqp_imp_canonical with (1 := cs) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.