proposition: Theorem mults_dist2 : forall (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)).
proof: Proof. Proof using os minusA invA divA cs A1. 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.