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