proposition: Theorem foreigner_red : forall (a b : poly A0 eqA ltM) (P : list (poly A0 eqA ltM)), foreigner a b -> In a P -> In b P -> red (spolyp a b) P.
proof: Proof. intros a b; case a; case b. intros x; case x. simpl in |- *; auto. unfold red in |- *; simpl in |- *; auto. intros a0 l c x0; case x0. unfold red in |- *; simpl in |- *; auto. unfold red in |- *; simpl in |- *; auto. intros a1 l0 c0 P H' H'0 H'1. unfold LetP in |- *; simpl in |- *; auto. apply reducestar_eqp_com with (1 := cs) (p := spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec (pX a0 l) (pX a1 l0) c c0) (q := pO A n); auto. apply spoly_Reducestar_ppc with (1 := cs); auto. change (inPolySet A A0 eqA n ltM (s2p A A0 eqA n ltM (mks A A0 eqA n ltM (pX a1 l0) c0)) P) in |- *. apply in_inPolySet; auto. red in |- *; intros H'3; inversion H'3; auto. change (inPolySet A A0 eqA n ltM (s2p A A0 eqA n ltM (mks A A0 eqA n ltM (pX a0 l) c)) P) in |- *. apply in_inPolySet; auto. red in |- *; intros H'3; inversion H'3; auto. apply spolyf_canonical with (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)