proposition: Theorem T1_multTerm_r : forall a b : Term, eqTerm a T1 -> eqTerm b (multTerm b a).
proof: Proof. Proof using plusA minusA invA divA cs A0. intros a b; case a; case b; simpl in |- *; auto. intros a0 m a1 m0 H'; elim H'; intros H'0 H'1; rewrite H'1; clear H'. split; auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA a0 A1); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA A1 a0); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); apply multA_A1_l with (1 := cs); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); auto. apply sym_eq; unfold M1 in |- *; apply mult_mon_zero_r. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)