proposition: Theorem eqTerm_multTerm_imp_eqTerm : forall a b c : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) c -> eqTerm (A:=A) eqA (n:=n) (multTerm (A:=A) multA (n:=n) c a) (multTerm (A:=A) multA (n:=n) c b) -> eqTerm (A:=A) eqA (n:=n) a b.
proof: Proof. Proof using plusA minusA invA divA cs A1. intros a b c nZc H'0. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := divTerm (multTerm (A:=A) multA (n:=n) c a) nZc); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm c nZc) a); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) a); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm c nZc) a); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := divTerm (multTerm (A:=A) multA (n:=n) c b) nZc); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm c nZc) b); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) b); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)