proposition: Theorem eqT_divTerm_plusTerm : forall (a b c : Term A n) (nZc : ~ zeroP (A:=A) A0 eqA (n:=n) c), eqT a b -> eqTerm (A:=A) eqA (n:=n) a (multTerm (A:=A) multA (n:=n) (divTerm a nZc) c) -> eqTerm (A:=A) eqA (n:=n) b (multTerm (A:=A) multA (n:=n) (divTerm b nZc) c) -> eqTerm (A:=A) eqA (n:=n) (divTerm (plusTerm (A:=A) plusA (n:=n) a b) nZc) (plusTerm (A:=A) plusA (n:=n) (divTerm a nZc) (divTerm b nZc)).
proof: Proof. Proof using minusA invA cs A1. intros a b c; case a; case b; case c; simpl in |- *; auto. intros a0 m a1 m0 a2 m1 nZc H' H'0 H'1; split; auto. case H'1; intros H'3 H'4; clear H'1. case H'0; intros H'2 H'5; clear H'0. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA (plusA (multA (divA a2 a0 nZc) a0) (multA (divA a1 a0 nZc) a0)) a0 nZc); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA (multA (plusA (divA a2 a0 nZc) (divA a1 a0 nZc)) a0) a0 nZc); auto. apply divA_eqA_comp with (1 := cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := plusA (multA a0 (divA a2 a0 nZc)) (multA a0 (divA a1 a0 nZc))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA a0 (plusA (divA a2 a0 nZc) (divA a1 a0 nZc))); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (plusA (divA a2 a0 nZc) (divA a1 a0 nZc)) (divA a0 a0 nZc)); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA (multA a0 (plusA (divA a2 a0 nZc) (divA a1 a0 nZc))) a0 nZc); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (divA a0 a0 nZc) (plusA (divA a2 a0 nZc) (divA a1 a0 nZc))); auto. apply divA_multA_comp_r with (1 := cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (plusA (divA a2 a0 nZc) (divA a1 a0 nZc)) A1); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. apply multA_eqA_comp with (1 := cs); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. apply divA_A1 with (1 := cs); auto. apply multA_A1_r with (1 := cs); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)