proposition: Theorem normalise_series_add_shift : ∀ s n m k, (normalise_series (n + m) k (series_shift m s) = normalise_series n k s)%ser.
proof: Proof. intros s n m k. unfold normalise_series. constructor; intros i; simpl. destruct (lt_dec (n + m + i * Pos.to_nat k) m) as [H₂| H₂]. rewrite Nat.add_shuffle0, Nat.add_comm in H₂. apply Nat.nle_gt in H₂. exfalso; apply H₂. apply Nat.le_add_r. rewrite Nat.add_comm, Nat.add_assoc, Nat.add_sub. rewrite Nat.add_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add