Require Export Pplus.
Section Pmults.
Load "hCoefStructure".
Load "hOrderStructure".
Load "hPlus".
Set Implicit Arguments.
Unset Strict Implicit.

Definition mults : Term A n → list (Term A n) → list (Term A n).
intros a p; elim p; clear p.
exact (pO A n).
intros b p1 p'1.
exact (pX (multTerm (A:=A) multA (n:=n) a b) p'1).
Defined.
Set Strict Implicit.
Unset Implicit Arguments.
Hint Resolve multTerm_eqT.
Hint Resolve invTerm_eqT.
Hint Resolve T1_is_min_ltT.

Lemma mults_order_l :
 ∀ l m1 m2,
 ¬ zeroP (A:=A) A0 eqA (n:=n) m1 ->
 canonical A0 eqA ltM (pX m2 l) →
 canonical A0 eqA ltM (pX (multTerm (A:=A) multA (n:=n) m1 m2) (mults m1 l)).
intros l; elim l; simpl in |- *; auto.
intros m1 m2 H' H'0.
apply canonicalp1; auto.
red in |- *; intros H'1; apply H'.
elim multTerm_zeroP_div with (1 := cs) (a := m1) (b := m2); auto; intros H'5.
absurd (zeroP (A:=A) A0 eqA (n:=n) m2); auto.
apply canonical_nzeroP with (ltM := ltM) (p := pO A n); auto.
intros a l0 H' m1 m2 H'0 H'1.
apply canonical_cons; auto.
apply multTerm_ltT_l; auto.
apply (canonical_pX_order A A0 eqA) with (l := l0); auto.
red in |- *; intros H'2; apply H'0.
elim multTerm_zeroP_div with (1 := cs) (a := m1) (b := m2); auto; intros H'5.
absurd (zeroP (A:=A) A0 eqA (n:=n) m2); auto.
apply canonical_nzeroP with (ltM := ltM) (p := pX a l0); auto.
apply H'; auto.
apply canonical_imp_canonical with (a := m2); auto.
Qed.

Lemma canonical_mults :
 ∀ m l,
 ¬ zeroP (A:=A) A0 eqA (n:=n) m →
 canonical A0 eqA ltM l → canonical A0 eqA ltM (mults m l).
intros m l; elim l; simpl in |- *; auto.
intros a l0 H' H'0 H'1.
apply mults_order_l; auto.
Qed.

Lemma canonical_mults_inv :
 ∀ (p : list (Term A n)) (a : Term A n),
 ¬ zeroP (A:=A) A0 eqA (n:=n) a →
 canonical A0 eqA ltM (mults a p) → canonical A0 eqA ltM p.
intros p; elim p; simpl in |- *; auto.
intros a l; case l; simpl in |- *; auto.
intros H' a0 H'0 H'1.
change (canonical A0 eqA ltM (pX a (pO A n))) in |- *; apply canonicalp1;
 auto.
red in |- *; intros H'2;
 absurd (zeroP (A:=A) A0 eqA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a));
 auto.
apply canonical_nzeroP with (ltM := ltM) (p := pO A n); auto.
intros a0 l0 H' a1 H'0 H'1.
change (canonical A0 eqA ltM (pX a (pX a0 l0))) in |- ×.
apply canonical_cons; auto.
case (ltT_dec A n ltM ltM_dec a0 a);
 [ intros temp; case temp; clear temp | idtac ]; intros H;
 auto.
absurd
 (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a)
    (multTerm (A:=A) multA (n:=n) a1 a0)); auto.
apply ltT_not_ltT; auto.
apply (canonical_pX_order A A0 eqA) with (l := mults a1 l0); auto.
apply multTerm_ltT_l with (1 := os); auto.
absurd
 (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a0)
    (multTerm (A:=A) multA (n:=n) a1 a)); auto.
apply (canonical_pX_order A A0 eqA) with (l := mults a1 l0); auto.
red in |- *; intros H'2;
 absurd (zeroP (A:=A) A0 eqA (n:=n) (multTerm (A:=A) multA (n:=n) a1 a));
 auto.
apply canonical_nzeroP with (ltM := ltM) (p := mults a1 l0); auto.
apply canonical_skip_fst with (b := multTerm (A:=A) multA (n:=n) a1 a0); auto.
apply H' with (a := a1); auto.
apply canonical_imp_canonical with (a := multTerm (A:=A) multA (n:=n) a1 a);
 auto.
Qed.

Set Implicit Arguments.
Unset Strict Implicit.

Definition tmults : Term A n → list (Term A n) → list (Term A n).
intros a; case (zeroP_dec A A0 eqA eqA_dec n a); intros Z0.
intros H'; exact (pO A n).
intros p; exact (mults a p).
Defined.
Set Strict Implicit.
Unset Implicit Arguments.

Theorem tmults_zerop_eqp_pO :
 ∀ p a,
 zeroP (A:=A) A0 eqA (n:=n) a → eqP A eqA n (tmults a p) (pO A n).
intros p a; unfold tmults in |- *; case (zeroP_dec A A0 eqA eqA_dec n a);
 auto.
intros H' H'0; elim H'; auto.
Qed.

Theorem mults_eqp_pO_pO :
 ∀ p a, eqP A eqA n p (pO A n) → eqP A eqA n (mults a p) (pO A n).
unfold pO in |- *; intros p a H'; inversion H'; auto.
Qed.


Theorem eqp_invT1_pO_is_pO :
 ∀ p : list (Term A n),
 eqP A eqA n (mults (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p) (pO A n) →
 eqP A eqA n p (pO A n).
intros p; case p; simpl in |- *; auto.
intros a l H'; inversion H'.
Qed.

Theorem mults_eqp_zpO :
 ∀ a : Term A n,
 ¬ zeroP (A:=A) A0 eqA (n:=n) a →
 ∀ p : list (Term A n),
 eqP A eqA n (mults a p) (pO A n) → eqP A eqA n p (pO A n).
intros a H' p; elim p; simpl in |- *; auto.
intros a0 l H'0 H'1; inversion H'1; auto.
Qed.

Theorem mults_dist1 :
 ∀ p a b,
 eqT a b →
 ¬ zeroP (A:=A) A0 eqA (n:=n) a →
 ¬ zeroP (A:=A) A0 eqA (n:=n) b →
 ¬ zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) →
 canonical A0 eqA ltM p →
 eqP A eqA n (mults (plusTerm (A:=A) plusA (n:=n) a b) p)
   (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
      (mults a p) (mults b p)).
intros p; elim p; simpl in |- *; auto.
intros; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n);
 apply p0_pluspf_l with (1 := cs); auto.
intros a l H' a0 b H'0 H'1 H'2 H'3 H'4.
cut (canonical A0 eqA ltM l); try apply canonical_imp_canonical with (a := a);
 auto; intros C0.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pX
            (plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)
               (multTerm (A:=A) multA (n:=n) b a))
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec (mults a0 l) (mults b l)));
 auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pX
            (plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)
               (multTerm (A:=A) multA (n:=n) b a))
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec (mults a0 l) (mults b l)));
 auto.
apply (eqpP1 _ eqA n); auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply multTerm_plusTerm_dist_l with (1 := cs); auto.
apply pluspf_inv3b with (1 := cs); auto.
red in |- *; intros H'5;
 absurd
  (zeroP (A:=A) A0 eqA (n:=n)
     (multTerm (A:=A) multA (n:=n) (plusTerm (A:=A) plusA (n:=n) a0 b) a));
 auto.
red in |- *; intros H'6.
elim
 multTerm_zeroP_div
  with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a0 b) (b := a);
 auto.
intros H'7; absurd (zeroP (A:=A) A0 eqA (n:=n) a); auto.
apply canonical_nzeroP with (ltM := ltM) (p := l); auto.
apply
 zeroP_comp_eqTerm
  with
    (1 := cs)
    (a := plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a)
            (multTerm (A:=A) multA (n:=n) b a)); auto.
apply multTerm_plusTerm_dist_l with (1 := cs); auto.
Qed.

Theorem mults_dist2 :
 ∀ (p : list (Term A n)) (a b : Term A n),
 eqT a b →
 ¬ zeroP (A:=A) A0 eqA (n:=n) a →
 ¬ zeroP (A:=A) A0 eqA (n:=n) b →
 zeroP (A:=A) A0 eqA (n:=n) (plusTerm (A:=A) plusA (n:=n) a b) →
 canonical A0 eqA ltM p →
 eqP A eqA n (pO A n)
   (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
      (mults a p) (mults b p)).
intros p; elim p; simpl in |- *; auto.
intros; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
intros a l H' a0 b H'0 H'1 H'2 H'3 H'4.
cut (canonical A0 eqA ltM l); try apply canonical_imp_canonical with (a := a);
 auto; intros C0.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
            (mults a0 l) (mults b l)); auto.
apply pluspf_inv3a with (1 := cs); auto.
apply
 zeroP_comp_eqTerm
  with
    (1 := cs)
    (a := multTerm (A:=A) multA (n:=n) (plusTerm (A:=A) plusA (n:=n) a0 b) a);
 auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply multTerm_plusTerm_dist_l with (1 := cs); auto.
Qed.

Theorem mults_T1 :
 ∀ (p : list (Term A n)) (a : Term A n),
 eqTerm (A:=A) eqA (n:=n) a (T1 A1 n) → eqP A eqA n (mults a p) p.
intros p; elim p; auto.
simpl in |- *; auto.
intros a l H a0 H0;
 change
   (eqP A eqA n (pX (multTerm (A:=A) multA (n:=n) a0 a) (mults a0 l))
      (pX a l)) in |- *; auto.
apply (eqpP1 A eqA n); auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); apply T1_multTerm_l with (1 := cs);
 auto.
Qed.

Theorem mults_invTerm :
 ∀ (p : list (Term A n)) (a : Term A n),
 eqTerm (A:=A) eqA (n:=n) a (T1 A1 n) →
 eqP A eqA n
   (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p
      (mults (invTerm (A:=A) invA (n:=n) a) p)) (pO A n).
intros p; elim p; simpl in |- *; auto.
intros a l H' a0 H'0.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
            l (mults (invTerm (A:=A) invA (n:=n) a0) l));
 auto.
change
  (eqP A eqA n
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l)
        (pX (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) a0) a)
           (mults (invTerm (A:=A) invA (n:=n) a0) l)))
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l
        (mults (invTerm (A:=A) invA (n:=n) a0) l)))
 in |- ×.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply pluspf_inv3a with (1 := cs);
 auto.
apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) a0 a); auto.
apply (T1_eqT _ A1 eqA); auto.
apply
 zeroP_comp_eqTerm
  with
    (1 := cs)
    (a := plusTerm (A:=A) plusA (n:=n) a (invTerm (A:=A) invA (n:=n) a));
 auto.
apply plusTerm_invTerm_zeroP with (1 := cs); auto.
apply plusTerm_comp_r with (1 := cs); auto.
change
  (eqT a (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) a0) a))
 in |- ×.
apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) a);
 auto.
apply (T1_eqT _ A1 eqA); auto.
apply multTerm_eqT; auto.
apply (eqT_trans A n) with (y := a0); auto.
apply (eqT_sym A n); auto.
apply (eqTerm_imp_eqT A eqA); auto.
apply
 (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := invTerm (A:=A) invA (n:=n)
            (multTerm (A:=A) multA (n:=n) a (T1 A1 n)));
 auto.
apply
 (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n)
  with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) a a0));
 auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply eqTerm_invTerm_comp with (1 := cs); auto.
apply
 (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n)
  with (y := invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) a0 a));
 auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply mult_invTerm_com with (1 := cs); auto.
Qed.

Theorem mults_multTerm :
 ∀ (p : list (Term A n)) (a b : Term A n),
 eqP A eqA n (mults (multTerm (A:=A) multA (n:=n) a b) p)
   (mults a (mults b p)).
intros p; elim p; simpl in |- *; auto.
intros a l H a0 b; apply (eqpP1 A eqA n); auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply multTerm_assoc with (1 := cs); auto.
Qed.

Theorem mults_com :
 ∀ (p : list (Term A n)) (a b : Term A n),
 eqP A eqA n (mults (multTerm (A:=A) multA (n:=n) a b) p)
   (mults (multTerm (A:=A) multA (n:=n) b a) p).
intros p; elim p; simpl in |- *; auto.
Qed.

Theorem mults_comp :
 ∀ (a b : Term A n) (p q : list (Term A n)),
 eqTerm (A:=A) eqA (n:=n) a b →
 eqP A eqA n p q → eqP A eqA n (mults a p) (mults b q).
intros a b p q H' H'0; elim H'0; simpl in |- *; auto.
Qed.

Theorem mults_ltP_comp :
 ∀ (a : Term A n) (p q : list (Term A n)),
 ltP (A:=A) (n:=n) ltM p q → ltP (A:=A) (n:=n) ltM (mults a p) (mults a q).
intros a p q H'; elim H'; simpl in |- *; auto.
intros x y p0 q0 H'0; simpl in |- *; apply ltP_hd; auto.
apply multTerm_ltT_l with (1 := os); auto.
Qed.


Theorem multlm_comp_canonical :
 ∀ (p : list (Term A n)) (a b : Term A n),
 canonical A0 eqA ltM (pX a p) →
 ¬ zeroP (A:=A) A0 eqA (n:=n) b →
 canonical A0 eqA ltM (pX (multTerm (A:=A) multA (n:=n) b a) (mults b p)).
intros p a b H' H'0; generalize (canonical_mults b (pX a p)); simpl in |- *;
 auto.
Qed.
Hint Resolve multlm_comp_canonical.

Let ffst := fst (A:=list (Term A n)) (B:=list (Term A n)).

Let ssnd := snd (A:=list (Term A n)) (B:=list (Term A n)).

Let ppair := pair (A:=list (Term A n)) (B:=list (Term A n)).

Definition twoP_ind :
  ∀ P : list (Term A n) → list (Term A n) → Prop,
  (∀ p q : list (Term A n),
   (∀ r s : list (Term A n), lessP A n (r, s) (p, q) → P r s) → P p q) →
  ∀ p q : list (Term A n), P p q.
intros P H' p q; try assumption.
change
  ((fun pq : list (Term A n) × list (Term A n) ⇒ P (ffst pq) (ssnd pq))
     (p, q)) in |- ×.
cut (∃ x : list (Term A n) × list (Term A n), x = ppair p q).
unfold ppair in |- *; intros H'0; elim H'0; intros x E; rewrite <- E;
 clear H'0.
pattern x in |- *;
 apply
  well_founded_ind
   with
     (A := (list (Term A n) × list (Term A n))%type)
     (R := lessP A n)
     (1 := wf_lessP A n); auto.
intros x0 H'0; apply H'; auto.
intros r s H'1.
apply (H'0 (r, s)).
generalize H'1; case x0; simpl in |- *; auto.
∃ (ppair p q); auto.
Qed.

Theorem mults_dist_pluspf :
 ∀ (p q : list (Term A n)) (a : Term A n),
 canonical A0 eqA ltM p →
 canonical A0 eqA ltM q →
 ¬ zeroP (A:=A) A0 eqA (n:=n) a →
 eqP A eqA n
   (mults a
      (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p
         q))
   (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
      (mults a p) (mults a q)).
intros p q; pattern p, q in |- ×.
apply twoP_ind; simpl in |- *; auto.
intros p0; case p0; simpl in |- *; auto.
intros q0 H' a H'0 H'1 H'2.
apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults a q0); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pO A n) q0) q0) in |- *; auto.
change
  (eqP A eqA n (mults a q0)
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pO A n) (mults a q0))) in |- *; auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
intros a l q0.
case q0; simpl in |- *; auto.
intros H' a0 H'0 H'1 H'2.
apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults a0 (pX a l)); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l) (pO A n)) (pX a l)) in |- *; auto.
change
  (eqP A eqA n (mults a0 (pX a l))
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX (multTerm multA a0 a) (mults a0 l)) (pO A n)))
 in |- *; simpl in |- *; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n);
 auto.
intros a0 l0 H' a1 H'0 H'1 H'2; simpl in |- ×.
case (ltT_dec A n ltM ltM_dec a a0); [ intros H0; case H0; clear H0 | idtac ];
 intros H0.
cut
 (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a)
    (multTerm (A:=A) multA (n:=n) a1 a0)); [ intros Od0 | idtac ];
 auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := mults a1
            (pX a0
               (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
                  ltM_dec (pX a l) l0))); auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pX a0
        (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
           (pX a l) l0))
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l) (pX a0 l0))) in |- ×.
auto.
apply pluspf_inv2 with (1 := cs); auto.
simpl in |- ×.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pX (multTerm (A:=A) multA (n:=n) a1 a0)
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec (pX (multTerm (A:=A) multA (n:=n) a1 a) (mults a1 l))
               (mults a1 l0))); auto.
apply eqpP1; auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
            (mults a1 (pX a l)) (mults a1 l0)); auto.
apply H'; simpl in |- *; auto.
red in |- *; red in |- *; simpl in |- *; rewrite <- plus_n_Sm; auto.
apply canonical_imp_canonical with (a := a0); auto.
apply pluspf_inv2 with (1 := cs); auto.
apply multTerm_ltT_l; auto.
cut
 (ltT ltM (multTerm (A:=A) multA (n:=n) a1 a0)
    (multTerm (A:=A) multA (n:=n) a1 a)); [ intros Od0 | idtac ];
 auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := mults a1
            (pX a
               (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
                  ltM_dec l (pX a0 l0)))); auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pX a
        (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
           l (pX a0 l0)))
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l) (pX a0 l0))) in |- ×.
apply pluspf_inv1 with (1 := cs); auto.
simpl in |- ×.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pX (multTerm (A:=A) multA (n:=n) a1 a)
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec (mults a1 l)
               (pX (multTerm (A:=A) multA (n:=n) a1 a0) (mults a1 l0))));
 auto.
apply eqpP1; auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
            (mults a1 l) (mults a1 (pX a0 l0))); auto.
apply H'; simpl in |- *; auto.
red in |- *; red in |- *; simpl in |- *; auto.
apply canonical_imp_canonical with (a := a); auto.
apply pluspf_inv1 with (1 := cs); auto.
apply multTerm_ltT_l; auto.
cut
 (eqT (multTerm (A:=A) multA (n:=n) a1 a)
    (multTerm (A:=A) multA (n:=n) a1 a0)); [ intros Od0 | idtac ];
 auto.
case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a a0));
 intros Z0.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := mults a1
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec l l0)); auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l
        l0)
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l) (pX a0 l0))) in |- *; auto.
apply pluspf_inv3a with (1 := cs); auto.
cut
 (zeroP (A:=A) A0 eqA (n:=n)
    (plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a1 a)
       (multTerm (A:=A) multA (n:=n) a1 a0))); [ intros Od1 | idtac ];
 auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
            (mults a1 l) (mults a1 l0)); auto.
apply H'; simpl in |- *; auto.
red in |- *; red in |- *; simpl in |- *; rewrite <- plus_n_Sm; auto.
apply canonical_imp_canonical with (a := a); auto.
apply canonical_imp_canonical with (a := a0); auto.
apply pluspf_inv3a with (1 := cs); auto.
apply
 zeroP_comp_eqTerm
  with
    (1 := cs)
    (a := multTerm (A:=A) multA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a a0)).
apply zeroP_multTerm_r with (1 := cs); auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply multTerm_plusTerm_dist_r with (1 := cs); auto.
cut
 (¬
  zeroP (A:=A) A0 eqA (n:=n)
    (plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a1 a)
       (multTerm (A:=A) multA (n:=n) a1 a0))); [ intros Od1 | idtac ];
 auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := mults a1
            (pX (plusTerm (A:=A) plusA (n:=n) a a0)
               (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
                  ltM_dec l l0))); auto.
apply mults_comp; auto.
change
  (eqP A eqA n
     (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
        (pX a l) (pX a0 l0))
     (pX (plusTerm (A:=A) plusA (n:=n) a a0)
        (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec
           l l0))) in |- ×.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply pluspf_inv3b with (1 := cs);
 auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply
 (eqp_trans _ _ _ _ _ _ _ _ _ cs n)
  with
    (y := pX
            (plusTerm (A:=A) plusA (n:=n) (multTerm (A:=A) multA (n:=n) a1 a)
               (multTerm (A:=A) multA (n:=n) a1 a0))
            (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM)
               ltM_dec (mults a1 l) (mults a1 l0)));
 auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply pluspf_inv3b with (1 := cs);
 auto.
simpl in |- ×.
apply eqpP1; auto.
apply multTerm_plusTerm_dist_r with (1 := cs); auto.
apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto.
apply H'; simpl in |- *; auto.
red in |- *; red in |- *; simpl in |- *; rewrite <- plus_n_Sm; auto.
apply canonical_imp_canonical with (a := a); auto.
apply canonical_imp_canonical with (a := a0); auto.
apply
 nzeroP_comp_eqTerm
  with
    (1 := cs)
    (a := multTerm (A:=A) multA (n:=n) a1 (plusTerm (A:=A) plusA (n:=n) a a0));
 auto.
apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n);
 apply multTerm_plusTerm_dist_r with (1 := cs); auto.
Qed.
Hint Resolve mults_dist_pluspf.

Definition smults : Term A n → poly A0 eqA ltM → poly A0 eqA ltM.
intros a sp1.
case sp1.
intros p1 H'1; ∃ (tmults a p1); auto.
unfold tmults in |- *; case (zeroP_dec A A0 eqA eqA_dec n a); simpl in |- *;
 auto.
intros; apply canonical_mults; auto.
Defined.

End Pmults.