proposition: Theorem divPp_divpf : forall (a : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a) (p : list (Term A n)), canonical A0 eqA ltM p -> divPp a p -> eqP A eqA n p (mults (A:=A) multA (n:=n) a (divpf a nZa p)).
proof: Proof. Proof using os minusA invA cs A1. intros a nZa p; elim p; simpl in |- *; auto. intros a0 l H' H'0 H'1; elim H'1; intros H'2 H'3; clear H'1. cut (canonical A0 eqA ltM l); [ intros Op0 | apply canonical_imp_canonical with (a := a0) ]; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a (pX (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a0 (b:=a) nZa) (pO A n))) (mults (A:=A) multA (n:=n) a (divpf a nZa l))). 2: apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a (pX (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a0 (b:=a) nZa) (pO A n))) l). simpl in |- *. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pX (multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a0 (b:=a) nZa) a) (pO A n)) l). apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pX a0 (pO A n)) l). change (eqP A eqA n (pX a0 l) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pX a0 (pO A n)) l)) in |- *; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pX a0 (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pO A n) l)). apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. rewrite pluspf_inv1_eqa; auto. apply canonicalp1; auto. apply (canonical_nzeroP A A0 eqA n ltM) with (p := l); auto. inversion H'2; auto. auto. auto. Qed.