proposition: Theorem ps_mul_0_l : ∀ ps, (0 * ps = 0)%ps.
proof: Proof. intros ps. constructor. unfold normalise_ps; simpl. unfold cm_factor; simpl. rewrite series_stretch_series_0. rewrite series_mul_0_l. rewrite series_order_series_0. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat