proposition: Theorem divP_trans : transitive (Term A n) divP.
proof: Proof. Proof using plusA minusA invA cs A1. red in |- *; intros a b c H' H'0. cut (~ zeroP (A:=A) A0 eqA (n:=n) c); [ intros nZc | auto ]. apply divTerm_def with (nZb := nZc); auto. apply divP_inv1 with (b := b); auto. 2: apply divP_inv2 with (a := b); auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) b); [ intros nZb | auto ]. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) (divTerm a nZb) (divTerm b nZc)) c); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm a nZb) (multTerm (A:=A) multA (n:=n) (divTerm b nZc) c)); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := multTerm (A:=A) multA (n:=n) (divTerm a nZb) b); auto. apply eqTerm_multTerm_comp with (1 := cs); auto. inversion H'0; inversion H'. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := divTerm (multTerm (A:=A) multA (n:=n) (divTerm a nZb) b) nZc); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply divTerm_multTerm_l; auto. apply eqTerm_divTerm_comp; auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (1 := H4); auto. apply divP_inv2 with (a := a); auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)