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