proposition: Theorem series_stretch_1 : ∀ α (r : ring α) s, (series_stretch 1 s = s)%ser.
proof: Proof. intros α r s. unfold series_stretch; simpl. constructor; intros i; simpl. rewrite divmod_div, Nat.div_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series