proposition: Theorem series_nth_add_shift : ∀ s i n, (series_shift n s) .[i + n] = s .[i].
proof: Proof. intros s i n; simpl. rewrite Nat.add_sub. destruct (lt_dec (i + n) n) as [H| H]; [ idtac | reflexivity ]. apply Nat.lt_add_lt_sub_r in H. rewrite Nat.sub_diag in H. exfalso; revert H; apply Nat.nlt_0_r. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series