proposition: Theorem series_shift_left_shift : ∀ s n, series_order s 0 = fin n → (series_shift n (series_left_shift n s) = s)%ser.
proof: Proof. intros s n Hn. apply series_order_iff in Hn. simpl in Hn. destruct Hn as (Hz, Hnz). constructor; intros i; simpl. destruct (lt_dec i n) as [H₁| H₁]. apply Hz in H₁. symmetry; assumption. apply Nat.nlt_ge in H₁. rewrite Nat.add_sub_assoc; [ idtac | assumption ]. rewrite Nat.add_comm, Nat.add_sub; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series