proposition: Theorem mults_pO : forall (p : list (Term A n)) (a b : Term A n), eqT a b -> zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) -> eqP A eqA n (pO A n) (minuspf (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) b p)).
proof: Proof. Proof using plusA os divA cs. intros p; elim p. simpl in |- *; auto. intros; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a l H' a0 b H'0 H'1; simpl in |- *. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := minuspf (mults (A:=A) multA (n:=n) a0 l) (mults (A:=A) multA (n:=n) b l)); auto. apply minuspf_inv3a; auto. apply zeroP_comp_eqTerm with (1 := cs) (a := multTerm (A:=A) multA (n:=n) (minusTerm (A:=A) minusA (n:=n) a0 b) a); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply multTerm_minusTerm_dist_l with (1 := cs); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)