proposition: Theorem divP_minusTerm_comp : forall a b c : Term A n, divP A A0 eqA multA divA n a c -> divP A A0 eqA multA divA n b c -> eqT a b -> ~ zeroP (A:=A) A0 eqA (n:=n) (minusTerm (A:=A) minusA (n:=n) a b) -> divP A A0 eqA multA divA n (minusTerm (A:=A) minusA (n:=n) a b) c.
proof: Proof. Proof using plusA invA cs A1. intros a b c H' H'0 H'1 H'2. apply divP_eqTerm_comp with (a := plusTerm (A:=A) plusA (n:=n) a (invTerm (A:=A) invA (n:=n) b)) (1 := cs); auto. apply divP_plusTerm with (1 := cs); auto. apply (eqT_trans A n) with (1 := H'1); auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := minusTerm (A:=A) minusA (n:=n) a b); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.