proposition: Theorem divpf_canonical : forall (a : Term A n) (p : list (Term A n)) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), canonical A0 eqA ltM p -> canonical A0 eqA ltM (divpf a nZa p).
proof: Proof. Proof using os multA minusA invA cs A1. intros a p; elim p; simpl in |- *; auto. intros a0 l H' H'0 H'1. apply canonical_pluspf; auto. apply canonicalp1; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); auto. apply (canonical_nzeroP A A0 eqA n ltM) with (p := l); auto. apply H'; auto. apply canonical_imp_canonical with (a := a0); auto. Qed.