proposition: Theorem series_nth_mul_shrink : ∀ (s : power_series α) k i, s .[Pos.to_nat k * i] = (series_shrink k s) .[i].
proof: Proof. intros s k i; simpl. rewrite Nat.mul_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series