proposition: Theorem spolyf_com : forall (a b : list (Term A n)) (Ca : canonical A0 eqA ltM a) (Cb : canonical A0 eqA ltM b), eqP A eqA n (spolyf a b Ca Cb) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (spolyf b a Cb Ca)).
proof: Proof. Proof using plusA os cs. intros a b; case a; case b; simpl in |- *; auto. intros a0 l a1 l0 Cpxa0 Cpxa1. cut (~ zeroP (A:=A) A0 eqA (n:=n) a0); [ intros nZa0 | apply canonical_nzeroP with (ltM := ltM) (p := l); auto ]. cut (~ zeroP (A:=A) A0 eqA (n:=n) a1); [ intros nZa1 | apply canonical_nzeroP with (ltM := ltM) (p := l0); auto ]. change (eqP A eqA n (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)))) in |- *. cut (canonical A0 eqA ltM l); [ intros Op1 | apply canonical_imp_canonical with (a := a0); auto ]. cut (canonical A0 eqA ltM l0); [ intros Op2 | apply canonical_imp_canonical with (a := a1); auto ]. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))); [ auto | idtac ]. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (T1 A1 n) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))). apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply eqp_pluspf_com with (1 := cs); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n))) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))); [ apply eqp_pluspf_com with (1 := cs); auto | idtac ]. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (multTerm (A:=A) multA (n:=n) (T1 A1 n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)))) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))); [ apply eqp_pluspf_com with (1 := cs); auto | idtac ]. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (invTerm (A:=A) invA (n:=n) (T1 A1 n))) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))); [ apply eqp_pluspf_com with (1 := cs); auto; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto | idtac ]. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0))) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))); [ apply eqp_pluspf_com with (1 := cs); auto | idtac ]. apply canonical_mults with (1 := cs); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l))). apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply mults_dist_pluspf with (1 := cs); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a1 a0) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0)))). apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply mults_comp with (1 := cs); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a0) (canonical_nzeroP A A0 eqA n ltM a0 l Cpxa1)) l) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) (ppc (A:=A) A1 (n:=n) a0 a1) (b:=a1) (canonical_nzeroP A A0 eqA n ltM a1 l0 Cpxa0)) l0))); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply eqp_pluspf_com with (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.