proposition: Theorem ps_zero_monom_eq : ∀ q, (ps_monom 0%K q = 0)%ps.
proof: Proof. intros q. unfold ps_zero, ps_monom; simpl. setoid_replace (series (λ i, if zerop i then 0%K else 0%K)) with 0%ser. constructor. unfold normalise_ps; simpl. rewrite zero_series_order; reflexivity. constructor; intros i; simpl. destruct (zerop i); reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series