proposition: Lemma spolyp_cons_genPcP : forall (aP R Q : list _) (i : poly A0 eqA ltM), genPcP i aP R Q -> ~ BuchAux.zerop A A0 eqA n ltM i -> forall b : poly A0 eqA ltM, In b aP -> ~ BuchAux.zerop A A0 eqA n ltM b -> exists c : poly A0 eqA ltM, In c aP /\ (In (spolyp A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os i c) Q \/ red A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec (spolyp A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os i c) (addEnd A A0 eqA n ltM i aP)) /\ divp A A0 eqA multA divA n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i b) c.
proof: Proof. intros aP R Q i H' H'0 b H'1 H'2. lapply (spolyp_cons_genPcP0 aP R Q i); [ intros H'7; lapply H'7; [ intros H'8; elim (H'8 b); [ intros c E; elim E; intros H'12 H'13; elim H'13; intros H'14 H'15; elim H'14; [ intros H'16; clear H'14 H'13 E H'7 | intros H'16; clear H'14 H'13 E H'7 ] | clear H'7 | clear H'7 ] | clear H'7 ] | idtac ]; auto. exists c; split; [ idtac | split; [ left | idtac ] ]; auto. exists c; split; [ idtac | split; [ right | idtac ] ]; auto. apply foreigner_red; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)