proposition: Theorem series_left_shift_shift : ∀ s n m, (m ≤ n)%nat → (series_left_shift n (series_shift m s) = series_left_shift (n - m) s)%ser.
proof: Proof. intros s n m Hmn. constructor; intros i; simpl. destruct (lt_dec (n + i) m) as [H₁| H₁]. apply Nat.nle_gt in H₁. exfalso; apply H₁. transitivity n; [ assumption | apply Nat.le_add_r ]. apply Nat.nlt_ge in H₁. rewrite Nat.add_sub_swap; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series