proposition: Theorem series_order_stretch_0 : ∀ s k, series_order (series_stretch k s) 0 = (fin (Pos.to_nat k) * series_order s 0)%Nbar.
proof: Proof. intros s k. rewrite <- series_order_stretch. rewrite Nat.mul_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series