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