proposition: Theorem eq_ps_trans : transitive _ eq_ps.
proof: Proof. intros ps₁ ps₂ ps₃ H₁ H₂. induction H₁. inversion H₂; subst. constructor; etransitivity; eassumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series