proposition: Theorem series_stretch_const : ∀ k c, (series_stretch k (series_const c) = series_const c)%ser.
proof: Proof. intros k c. constructor; intros i; simpl. destruct (zerop (i mod Pos.to_nat k)) as [H| H]. apply Nat.mod_divides in H; auto with Arith. destruct H as (d, Hd); rewrite Hd. rewrite Nat.mul_comm. rewrite Nat.div_mul; auto with Arith. destruct d; [ reflexivity | idtac ]. rewrite Nat.mul_comm; simpl. rewrite <- Hd. destruct i; [ idtac | reflexivity ]. symmetry in Hd. apply Nat.mul_eq_0_r in Hd; auto with Arith; discriminate Hd. destruct i; [ simpl | reflexivity ]. rewrite Nat.mod_0_l in H; auto with Arith. exfalso; revert H; apply Nat.lt_irrefl. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series