proposition: Theorem stretch_shift_series_distr : ∀ kp n s, (series_stretch kp (series_shift n s) = series_shift (n * Pos.to_nat kp) (series_stretch kp s))%ser.
proof: Proof. intros kp n s. constructor; intros i; simpl. remember (Pos.to_nat kp) as k. assert (k ≠ O) as Hk by (subst k; apply Pos2Nat_ne_0). destruct (zerop (i mod k)) as [Hz| Hnz]. apply Nat.mod_divides in Hz; [ idtac | assumption ]. destruct Hz as (c, Hi); subst i. rewrite mult_comm. rewrite <- Nat.mul_sub_distr_r. rewrite Nat.div_mul; [ idtac | assumption ]. rewrite Nat.div_mul; [ idtac | assumption ]. rewrite Nat.mod_mul; [ simpl | assumption ]. destruct (lt_dec c n) as [H₁| H₁]. destruct (lt_dec (c * k) (n * k)) as [| H₂]; [ reflexivity | idtac ]. exfalso; apply H₂. apply Nat.mul_lt_mono_pos_r; [ idtac | assumption ]. rewrite Heqk; apply Pos2Nat.is_pos. destruct (lt_dec (c * k) (n * k)) as [H₂| ]; [ idtac | reflexivity ]. exfalso; apply H₁. apply Nat.mul_lt_mono_pos_r in H₂; [ assumption | idtac ]. rewrite Heqk; apply Pos2Nat.is_pos. destruct (lt_dec i (n * k)) as [| H₁]; [ reflexivity | idtac ]. destruct (zerop ((i - n * k) mod k)) as [H₂| ]; [ idtac | reflexivity ]. apply Nat.mod_divides in H₂; [ idtac | assumption ]. destruct H₂ as (c, Hc). destruct c. rewrite Nat.mul_0_r in Hc. apply Nat.sub_0_le in Hc. apply Nat.nlt_ge in H₁. apply le_antisym in Hc; [ idtac | assumption ]. subst i. rewrite Nat.mod_mul in Hnz; [ idtac | assumption ]. exfalso; revert Hnz; apply Nat.lt_irrefl. apply Nat.add_sub_eq_nz in Hc. rewrite Nat.mul_comm, <- Nat.mul_add_distr_l, Nat.mul_comm in Hc. subst i. rewrite Nat.mod_mul in Hnz; [ idtac | assumption ]. exfalso; revert Hnz; apply Nat.lt_irrefl. apply Nat.neq_mul_0. split; [ assumption | idtac ]. intros H; discriminate H. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series