proposition: Theorem series_stretch_stretch : ∀ a b s, (series_stretch (a * b) s = series_stretch a (series_stretch b s))%ser.
proof: Proof. intros ap bp s. unfold series_stretch; simpl. constructor; intros i; simpl. rewrite Pos2Nat.inj_mul. remember (Pos.to_nat ap) as a. remember (Pos.to_nat bp) as b. assert (a ≠ O) as Ha by (subst a; apply Pos2Nat_ne_0). assert (b ≠ O) as Hb by (subst b; apply Pos2Nat_ne_0). destruct (zerop (i mod (a * b))) as [Hz| Hnz]. apply Nat.mod_divides in Hz. destruct Hz as (c, Hz). subst i. rewrite Nat.mul_comm, Nat.div_mul. rewrite Nat.mul_assoc, Nat.mul_shuffle0. rewrite Nat.mod_mul; [ simpl | assumption ]. rewrite Nat.div_mul; [ simpl | assumption ]. rewrite Nat.mod_mul; [ simpl | assumption ]. rewrite Nat.div_mul; [ simpl | assumption ]. reflexivity. apply Nat.neq_mul_0; split; assumption. apply Nat.neq_mul_0; split; assumption. destruct (zerop (i mod a)) as [Hz| ]; [ idtac | reflexivity ]. apply Nat.mod_divides in Hz; [ idtac | assumption ]. destruct Hz as (c, Hz). subst i. rewrite Nat.mul_comm, Nat.div_mul; [ idtac | assumption ]. destruct (zerop (c mod b)) as [Hlt₂| ]; [ idtac | reflexivity ]. apply Nat.mod_divides in Hlt₂; [ idtac | assumption ]. destruct Hlt₂ as (c₂, Hlt₂). subst c. rewrite Nat.mul_assoc, Nat.mul_comm in Hnz. rewrite Nat.mod_mul in Hnz. exfalso; revert Hnz; apply lt_irrefl. apply Nat.neq_mul_0; split; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series