proposition: Theorem divTerm_invTerm_l : forall (a b : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), eqTerm (A:=A) eqA (n:=n) b (multTerm (A:=A) multA (n:=n) (divTerm b nZa) a) -> eqTerm (A:=A) eqA (n:=n) (divTerm (invTerm (A:=A) invA (n:=n) b) nZa) (invTerm (A:=A) invA (n:=n) (divTerm b nZa)).
proof: Proof. Proof using plusA minusA cs A1. intros a b; case a; case b; simpl in |- *; auto. intros d c A0' c0 nZA2 H'0; split; auto. case H'0; intros H'1 H'2; clear H'0. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA (invA (multA (divA d A0' nZA2) A0')) A0' nZA2); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := divA (multA (invA (divA d A0' nZA2)) A0') A0' nZA2); auto. apply divA_eqA_comp with (1 := cs); auto. apply (eqA_sym _ _ _ _ _ _ _ _ _ cs); apply multA_invA_com_l with (1 := cs); auto. apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (invA (divA d A0' nZA2)) (divA A0' A0' nZA2)); auto. apply divA_multA_comp_l with (1 := cs). apply (eqA_trans _ _ _ _ _ _ _ _ _ cs) with (y := multA (invA (divA d A0' nZA2)) A1); auto. apply multA_eqA_comp with (1 := cs); auto. apply divA_A1 with (1 := cs). apply multA_A1_r with (1 := cs). Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)