proposition: Theorem red_com : forall (a b : poly A0 eqA ltM) (aL : list (poly A0 eqA ltM)), red (spolyp a b) aL -> red (spolyp b a) aL.
proof: Proof. intros a b; case a; case b; simpl in |- *. unfold red in |- *; simpl in |- *. intros x Cx x0 Cx0 aL H'1; inversion H'1. cut (canonical A0 eqA ltM (spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec x x0 Cx Cx0)); [ intros Op1 | apply spolyf_canonical with (1 := cs) ]; auto. cut (canonical A0 eqA ltM (spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec x0 x Cx0 Cx)); [ intros Op2 | apply spolyf_canonical with (1 := cs) ]; auto. apply reducestar0; auto. apply reduceplus_eqp_com with (1 := cs) (p := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (spolyf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec x x0 Cx Cx0)) (q := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (pO A n)); auto. apply reduceplus_mults with (1 := cs); auto. inversion H; auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply spolyf_com with (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply spolyf_com with (1 := cs); auto. Qed.
imports: Buchberger(moreCoefStructure)