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