proposition: Lemma spolyp_cons_genPcP0 : 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 \/ foreigner A A0 A1 eqA multA n ltM i c) /\ 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'; elim H'; clear H' i aP R Q; simpl in |- *; auto. intros i L H' b H'0; elim H'0. intros L L1 L2 L3 a i H' H'0 H'1 H'2 b H'3 H'4. cut (incl L2 L1); [ intros incl0 | generalize (slicef_incl i a L1); unfold slicef in |- *; rewrite H' ]; auto. elim H'3; [ intros H'5; rewrite <- H'5; clear H'3 | intros H'5; clear H'3 ]; auto. exists a; split; [ idtac | split; [ left | idtac ] ]; auto. rewrite H'5; auto. apply zerop_ddivp_ppc; auto. elim (slice_inv i a L1 b); [ intros H'10 | intros H'10 | idtac ]; auto. rewrite H' in H'10; simpl in H'10; auto. lapply H'1; [ intros H'3; elim (H'3 b); [ intros c E; elim E; intros H'9 H'11; elim H'11; intros H'12 H'13; elim H'12; [ intros H'14; clear H'12 H'11 E H'1 | intros H'14; clear H'12 H'11 E H'1 ] | clear H'1 | clear H'1 ] | clear H'1 ]; auto. exists c; split; [ right | idtac ]; auto. exists c; split; [ idtac | split; [ right | idtac ] ]; auto. exists a; split; [ idtac | split ]; auto. intros L L1 L2 L3 a i H' H'0 H'1 H'2 b H'3 H'4. cut (incl L2 L1); [ intros incl0 | generalize (slicef_incl i a L1); unfold slicef in |- *; rewrite H' ]; auto. elim H'3; [ intros H'5; rewrite <- H'5; clear H'3 | intros H'5; clear H'3 ]; auto. elim (slice_cons i a L1 L2); [ intros H'8; elim H'8; intros c E; elim E; intros H'9 H'10; clear E H'8 | intros H'8 | idtac ]; auto. lapply H'1; [ intros H'3; elim (H'3 c); [ intros c0 E; elim E; intros H'11 H'12; elim H'12; intros H'13 H'14; elim H'13; [ intros H'15; clear H'13 H'12 E H'1 | intros H'15; clear H'13 H'12 E H'1 ] | clear H'1 | clear H'1 ] | clear H'1 ]; auto. exists c0; split; [ idtac | split; [ left | idtac ] ]; auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i c); auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. rewrite H'5; auto. exists c0; split; [ idtac | split; [ right | idtac ] ]; auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i c); auto. rewrite H'5; auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. rewrite <- H'5; auto. apply divp_nzeropr with (1 := H'10); auto. exists a; split; [ idtac | split; [ right | idtac ] ]; auto. rewrite H'5; auto. apply zerop_ddivp_ppc; auto. elim (slice_inv i a L1 b); [ intros H'10 | intros H'10 | idtac ]; auto. rewrite H' in H'10; simpl in H'10; auto. lapply H'1; [ intros H'3; elim (H'3 b); [ intros c E; elim E; intros H'9 H'11; elim H'11; intros H'12 H'13; elim H'12; [ intros H'14; clear H'12 H'11 E H'1 | intros H'14; clear H'12 H'11 E H'1 ] | clear H'1 | clear H'1 ] | clear H'1 ]; auto. exists c; split; [ right | idtac ]; auto. exists c; split; [ idtac | split; [ right | idtac ] ]; auto. elim (slice_cons i a L1 L2); [ intros H'8; elim H'8; intros c E; elim E; intros H'9 H'11; clear E H'8 | intros H'8 | idtac ]; auto. lapply H'1; [ intros H'3; elim (H'3 c); [ intros c0 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'1 | intros H'16; clear H'14 H'13 E H'1 ] | clear H'1 | clear H'1 ] | clear H'1 ]; auto. exists c0; split; [ idtac | split; [ left | idtac ] ]; auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i c); auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i a); auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. apply divp_nzeropr with (1 := H'10); auto. exists c0; split; [ idtac | split; [ right | idtac ] ]; auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i a); auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. apply (divp_trans _ _ _ _ _ _ _ _ _ cs n ltM) with (y := ppcp A A0 A1 eqA plusA invA minusA multA divA cs n ltM i c); auto. apply divP_ppc; auto. apply divp_ppc; auto. apply zerop_ddivp_ppc; auto. apply divp_nzeropr with (1 := H'10); auto. apply divp_nzeropr with (1 := H'11); auto. exists a; split; [ idtac | split; [ right | idtac ] ]; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)