proposition: Theorem ps_lap_eq_trans {α} {R : ring α} {K : field R} : transitive _ (@ps_lap_eq _ R K).
proof: Proof. intros la lb lc Hlab Hlbc. progress unfold ps_lap_eq; etransitivity; eassumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Puiseux_series Ps_add Ps_mul Ps_div