proposition: Theorem series_shrink_shrink : ∀ (s : power_series α) k₁ k₂, (series_shrink (k₁ * k₂) s = series_shrink k₁ (series_shrink k₂ s))%ser.
proof: Proof. intros s k₁ k₂. constructor; intros i; simpl. rewrite Pos2Nat.inj_mul, Nat.mul_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series