proposition: Theorem series_nth_shift_S : ∀ s n i, (series_shift n s) .[i] = (series_shift (S n) s) .[S i].
proof: Proof. intros s n i; simpl. destruct (lt_dec i n) as [H₁| H₁]. destruct (lt_dec (S i) (S n)) as [| H₂]; [ reflexivity | idtac ]. apply Nat.succ_lt_mono in H₁; contradiction. destruct (lt_dec (S i) (S n)) as [H₂| ]; [ idtac | reflexivity ]. apply Nat.succ_lt_mono in H₂; contradiction. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series