proposition: Theorem reduce_eqp_com : forall (Q : list (poly A0 eqA ltM)) (p q r s : list (Term A n)), reduce Q p q -> canonical A0 eqA ltM p -> eqP A eqA n p r -> eqP A eqA n q s -> reduce Q r s.
proof: Proof. Proof using plusA os cs. intros Q p q r s H'; generalize r s; clear r s; elim H'; auto. intros a b nZb p0 q0 r H'0 H'1 H'2 r0 s H'3 H'4 H'5. inversion_clear H'4. apply reducetop with (b := b) (nZb := nZb) (q := q0); auto. apply divP_eqTerm_comp with (1 := cs) (a := a); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p0 q0); auto. cut (canonical A0 eqA ltM p0); [ intros Cp0 | apply canonical_imp_canonical with (a := a); auto ]. apply eqp_spminusf_com with (1 := cs); auto. apply eqp_imp_canonical with (1 := cs) (p := p0); auto. apply canonical_imp_canonical with (a := b); auto. apply inPolySet_imp_canonical with (L := Q); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply divP_eqTerm_comp with (1 := cs) (a := a); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (2 := H'5); auto. intros a b p0 q0 H'0 H'1 H'2 r s H'3 H'4 H'5. inversion_clear H'4. inversion_clear H'5. apply reduceskip; auto. apply H'1; auto. apply canonical_imp_canonical with (a := a); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := a); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply (eqTerm_trans _ _ _ _ _ _ _ _ _ cs n) with (y := b); auto. Qed.