proposition: Theorem spolyp_addEnd_genPcPf : forall (aP R Q : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), ~ BuchAux.zerop A A0 eqA n ltM a -> ~ BuchAux.zerop A A0 eqA n ltM b -> In b aP -> 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 a c) (genPcPf a aP 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 a c) (addEnd A A0 eqA n ltM a aP)) /\ divp A A0 eqA multA divA n ltM (ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM a b) c.
proof: Proof. intros aP H' Q a b H'0 H'1 H'2. unfold genPcPf in |- *. case (genPcPf0 a aP Q). intros x H'3. apply spolyp_cons_genPcP with (R := Q); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)