proposition: Theorem genPcP_spolyp1 : forall (i : poly A0 eqA ltM) (L L1 L2 : list _), genPcP i L1 L L2 -> forall a : poly A0 eqA ltM, In a L2 -> (exists b : poly A0 eqA ltM, In b L1 /\ a = spolyp A A0 A1 eqA plusA invA minusA multA divA cs eqA_dec n ltM ltM_dec os i b) \/ In a L.
proof: Proof. intros i L L1 L2 H'; elim H'; clear H'; simpl in |- *; auto. intros L0 L3 L4 L5 a i0 H' H'0 H'1 a0 H'2. case (addEnd_cons A A0 eqA n ltM) with (1 := H'2); auto; intros H'7. rewrite H'7; auto. left; exists a; split; simpl in |- *; auto. elim (H'1 a0); auto. intros H'3; case H'3; intros b E; case E; intros H'4 H'5; rewrite H'5; clear E H'3. left; exists b; split; auto. right; try assumption. generalize (slicef_incl i0 a L3); unfold slicef in |- *; rewrite H'; auto. intros L0 L3 L4 L5 a i0 H' H'0 H'1 a0 H'2. elim (H'1 a0); [ intros H'5; elim H'5; intros b E; elim E; intros H'6 H'7; rewrite H'7; clear E H'5 | intros H'5 | idtac ]; auto. left; exists b; split; [ right | idtac ]; auto. generalize (slicef_incl i0 a L3); unfold slicef in |- *; rewrite H'; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)