proposition: Theorem divP_plusTerm : forall a b c : Term A n, divP a c -> divP b c -> eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) -> divP (plusTerm (A:=A) plusA (n:=n) a b) c.
proof: Proof. Proof using minusA invA cs A1. intros a b c H' H'0; inversion H'0; inversion H'. intros H'1 H'2; apply divTerm_def with (nZb := nZb0); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) (divTerm a nZb0) c) (multTerm (A:=A) multA (n:=n) (divTerm b nZb0) c)); auto. apply eqTerm_plusTerm_comp with (1 := cs); auto. apply multTerm_eqT; auto. apply eqT_divTerm; auto. apply (eqT_refl A n). apply (eqT_refl A n). apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (plusTerm (A:=A) plusA (n:=n) (divTerm a nZb0) (divTerm b nZb0)) c); auto. apply multTerm_plusTerm_dist_l with (1 := cs); auto. apply eqTerm_multTerm_comp with (1 := cs); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply eqT_divTerm_plusTerm; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)