proposition: Theorem series_order_shift_add : ∀ s m n, series_order (series_shift m s) (m + n) = series_order s n.
proof: Proof. intros s m n. remember (series_order s n) as v eqn:Hv . symmetry in Hv. apply series_order_iff in Hv. apply series_order_iff. destruct v as [v| ]. destruct Hv as (Hltz, Hnz). split. intros i Hiv. rewrite <- Nat.add_assoc, Nat.add_comm. rewrite series_nth_add_shift. apply Hltz; assumption. rewrite <- Nat.add_assoc, Nat.add_comm. rewrite series_nth_add_shift. assumption. intros i. rewrite <- Nat.add_assoc, Nat.add_comm. rewrite series_nth_add_shift. apply Hv. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series