proposition: Theorem eq_strong_trans α (r : ring α) : transitive _ eq_ps_strong.
proof: Proof. intros ps₁ ps₂ ps₃ H₁ H₂. induction H₁, H₂. constructor; etransitivity; eassumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series