proposition: Theorem series_shrink_stretch : ∀ s k, (series_shrink k (series_stretch k s) = s)%ser.
proof: Proof. intros s k. constructor; intros i; simpl. rewrite Nat.mod_mul; auto with Arith; simpl. rewrite Nat.div_mul; auto with Arith; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series