proposition: Theorem divpf_comp : forall (a b : Term A n) (p q : list (Term A n)), eqP A eqA n p q -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> eqTerm (A:=A) eqA (n:=n) a b -> forall (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b), eqP A eqA n (divpf a nZa p) (divpf b nZb q).
proof: Proof. Proof using os multA minusA invA cs A1. intros a b p q H'; elim H'; simpl in |- *; auto. intros ma mb p0 q0 H'0 H'1 H'2 H'3 H'4 H'5 H'6 H'7. cut (canonical A0 eqA ltM p0); [ intros Op1 | apply canonical_imp_canonical with (a := ma); auto ]. cut (canonical A0 eqA ltM q0); [ intros Op2 | apply canonical_imp_canonical with (a := mb); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) ma); [ intros Z0 | apply canonical_nzeroP with (ltM := ltM) (p := p0); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) mb); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := q0); auto ]. auto. Qed.