proposition: Theorem series_shrink_1 : ∀ s, (series_shrink 1 s = s)%ser.
proof: Proof. intros s. unfold series_shrink; simpl. constructor; intros n; simpl. rewrite Nat.mul_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series