proposition: Theorem mults_minusTerm : 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) -> canonical A0 eqA ltM p -> eqP A eqA n (mults (A:=A) multA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) p) (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 a b H H0 H1; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a l H' a0 b H'0 H'1 H'2; simpl in |- *; auto. cut (canonical A0 eqA ltM l); try apply canonical_imp_canonical with (a := a); auto; intros Z0; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX (minusTerm (A:=A) minusA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a) (multTerm (A:=A) multA (n:=n) b a)) (minuspf (mults (A:=A) multA (n:=n) a0 l) (mults (A:=A) multA (n:=n) b l))); auto. apply (eqpP1 A eqA); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply multTerm_minusTerm_dist_l with (1 := cs); auto. apply minuspf_inv3b; auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := multTerm (A:=A) multA (n:=n) (minusTerm (A:=A) minusA (n:=n) a0 b) a); auto. apply nzeroP_multTerm with (1 := cs); auto. apply (canonical_nzeroP A A0 eqA n ltM) with (p := l); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply multTerm_minusTerm_dist_l with (1 := cs); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)