(* week-10_integers.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 27 Jun 2025 *)

(* ********** *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith Bool ZArith.

(* ********** *)

Theorem binomial_expansion_at_rank_2 :
  forall x y : Z,
    ((x - y) * (x - y) = x * x - 2 * x * y + y * y)%Z.
Proof.
  intros x y.
  ring.
Qed.

(* ********** *)

Fixpoint Sigma0 (n : nat) (f : nat -> Z) : Z :=
  match n with
  | O =>
    f 0
  | S n' =>
    Sigma0 n' f + f (S n')
  end.

Lemma fold_unfold_Sigma0_O :
  forall (f : nat -> Z),
    Sigma0 0 f =
    f 0.
Proof.
  fold_unfold_tactic Sigma0.
Qed.

Lemma fold_unfold_Sigma0_S :
  forall (n' : nat)
         (f : nat -> Z),
    Sigma0 (S n') f =
    (Sigma0 n' f + f (S n'))%Z.
Proof.
  fold_unfold_tactic Sigma0.
Qed.

(* ********** *)

Theorem fundamental_for_int_valued_functions :
  forall (f : nat -> Z)
         (n : nat),
    Sigma0 n (fun i => (f (S i) - f i)%Z) = (f (S n) - f 0%nat)%Z.
Proof.
  intros f n.
  induction n as [ | n' IHn'].
  - rewrite -> fold_unfold_Sigma0_O.
    reflexivity.
  - rewrite -> fold_unfold_Sigma0_S.
    rewrite -> IHn'.
    ring.
Qed.

(* ********** *)

(* Exercise 05 *)

Theorem summation_by_parts_for_int_valued_functions : (* Abel's lemma *)
  forall (f g : nat -> Z)
         (n : nat),
    (Sigma0 n (fun i => f i * (g (S i) - g i)) + f 0%nat * g 0%nat + Sigma0 n (fun i => g (S i) * (f (S i) - f i)))%Z
    =
    (f (S n) * g (S n))%Z.
Proof.
  intros f g n.
  induction n as [ | n' IHn'].
  - rewrite ->2 fold_unfold_Sigma0_O.
    ring.
  - rewrite ->2 fold_unfold_Sigma0_S.
    remember (Sigma0 n' (fun i : nat => (f i * (g (S i) - g i))%Z)) as x eqn:X.
    remember (f 0%nat * g 0%nat)%Z as y eqn:Y.
    remember (Sigma0 n' (fun i : nat => (g (S i) * (f (S i) - f i))%Z)) as z eqn:Z.
    Search (_ * (_ - _))%Z.
    rewrite ->2 Z.mul_sub_distr_l.
    remember (f (S (S n')) * g (S (S n')))%Z as a eqn:A.
    remember (f (S n') * g (S (S n')) - f (S n') * g (S n'))%Z as b eqn:B.
    remember (g (S (S n')) * f (S (S n')) - g (S (S n')) * f (S n'))%Z as c eqn:C.
    rewrite -> (Z.add_shuffle0 x b y).
    rewrite -> (Z.add_assoc _ z c).
    rewrite -> (Z.add_shuffle0 (x + y) b z).
    rewrite -> IHn'.
    rewrite -> A.
    rewrite -> B.
    rewrite -> C.
    ring.
Qed.

(* ********** *)

Definition abs (n : Z) : Z :=
  if (n <? 0)%Z
  then 0 - n
  else n.

(* ********** *)

Theorem Dijkstra_s_abs :
  forall a b : Z,
    (abs a < b <-> a < b /\ 0 - a < b)%Z
    /\
    (a < abs b <-> a < b \/ a < 0 - b)%Z.
Proof.
  intros a b.
  split.
  - destruct (Ztrichotomy a 0) as [lt_a_0 | [eq_a_0 | lt_0_a]].
    + unfold abs.
      Search ((_ <? _) = true)%Z.
(* Z.ltb_lt: forall n m : Z, (n <? m)%Z = true <-> (n < m)%Z *)
      destruct (Z.ltb_lt a 0) as [S C].
      rewrite -> (C lt_a_0).
      split.
      * intro lt_0_minus_a_b.
        destruct (Ztrichotomy b 0) as [lt_b_0 | [eq_b_0 | lt_0_b]].
        ** Search ((_ < _ -> _ < _ -> _ < _)%Z).
(* Z.lt_trans: forall n m p : Z, (n < m)%Z -> (m < p)%Z -> (n < p)%Z *)
           Check (Z.lt_trans (0 - a) b 0 lt_0_minus_a_b lt_b_0). (* : (0 - a < 0)%Z*)
           Search (_ < _ -> _ + _ < _ + _)%Z.
(* Zplus_lt_compat_r: forall n m p : Z, (n < m)%Z -> (n + p < m + p)%Z *)
           assert (tmp := Zplus_lt_compat_r (0 - a) 0 a (Z.lt_trans (0 - a) b 0 lt_0_minus_a_b lt_b_0)).
           Search (_ - _ + _ = _)%Z.
(* Z.sub_simpl_r: forall n m : Z, (n - m + m)%Z = n *)
           rewrite -> (Z.sub_simpl_r 0 a) in tmp.
           rewrite -> Z.add_0_l in tmp.
           Check (Z.lt_trans 0 a 0 tmp lt_a_0). (* : (0 < 0)%Z *)
           Check Z.lt_irrefl. (* : forall x : Z, ~ (x < x)%Z *)
           contradiction (Z.lt_irrefl 0 (Z.lt_trans 0 a 0 tmp lt_a_0)).
        ** rewrite -> eq_b_0 in lt_0_minus_a_b.
           assert (tmp := Zplus_lt_compat_r (0 - a) 0 a lt_0_minus_a_b).
           rewrite -> (Z.sub_simpl_r 0 a) in tmp.
           rewrite -> Z.add_0_l in tmp.
           contradiction (Z.lt_irrefl 0 (Z.lt_trans 0 a 0 tmp lt_a_0)).
        ** split.
           *** assert (tmp : (a < 0 - a)%Z).
               { Check (Z.lt_trans a 0 (0 - a) lt_a_0). (* : (0 < 0 - a)%Z -> (a < 0 - a)%Z *)
                 Search (_ < _ - _)%Z.
(* Z.lt_add_lt_sub_r: forall n m p : Z, (n + p < m)%Z <-> (n < m - p)%Z *)
                 Check (Z.lt_add_lt_sub_r a 0 a).
                 destruct (Z.lt_add_lt_sub_r a 0 a) as [foo bar].
                 apply foo.
                 Search ((_ < _ -> _ < _ -> _ < _)%Z).
(* Z.add_lt_mono: forall n m p q : Z, (n < m)%Z -> (p < q)%Z -> (n + p < m + q)%Z *)
                 Check (Z.add_lt_mono a 0 a 0 lt_a_0 lt_a_0). (* : (a + a < 0 + 0)%Z *)
                 rewrite <- (Z.add_0_l 0).
                 exact (Z.add_lt_mono a 0 a 0 lt_a_0 lt_a_0). }
               exact (Z.lt_trans a (0 - a) b tmp lt_0_minus_a_b).
           *** exact lt_0_minus_a_b.
      * intros [_ ly].
        exact ly.
    + rewrite -> eq_a_0.
      unfold abs.
      Search ((_ <? _) = false)%Z.
(* Z.ltb_irrefl: forall x : Z, (x <? x)%Z = false *)
      rewrite -> (Z.ltb_irrefl 0).
      Search (_ - _ = 0)%Z.
(* Z.sub_diag: forall n : Z, (n - n)%Z = 0%Z *)
      rewrite -> (Z.sub_diag 0).
      split.
      * intro ly.
        split; exact ly.
      * intros [ly _].
        exact ly.
    + unfold abs.
      Search (_ > _ -> _ < _)%Z.
(* Z.gt_lt: forall n m : Z, (n > m)%Z -> (m < n)%Z *)
      Check (Z.gt_lt a 0 lt_0_a). (* : (0 < a)%Z *)
      Search (_ < _ -> _ <= _)%Z.
(* Z.lt_le_incl: forall n m : Z, (n < m)%Z -> (n <= m)%Z *)
      Check (Z.lt_le_incl 0 a (Z.gt_lt a 0 lt_0_a)). (* : (0 <= a)%Z *)
      Search ((_ <? _) = false)%Z.
(* Z.ltb_ge: forall x y : Z, (x <? y)%Z = false <-> (y <= x)%Z *)
      Check (Z.ltb_ge a 0).
      destruct (Z.ltb_ge a 0) as [foo bar].
      Check (bar (Z.lt_le_incl 0 a (Z.gt_lt a 0 lt_0_a))).
      rewrite -> (bar (Z.lt_le_incl 0 a (Z.gt_lt a 0 lt_0_a))).
      split.
      * intro lt_a_b.
        split.
        ** exact lt_a_b.
        ** assert (lt_0_minus_a_0 :
                     (0 - a < a)%Z).
           { assert (gt_a_0 := lt_0_a).
             clear lt_0_a.
             assert (lt_0_a := Z.gt_lt a 0 gt_a_0).
             Search (_ - _ < _)%Z.
(* Z.sub_lt_mono: forall n m p q : Z, (n < m)%Z -> (q < p)%Z -> (n - p < m - q)%Z *)
             Check (Z.sub_lt_mono 0 a a 0 lt_0_a lt_0_a). (* : (0 - a < a - 0)%*Z *)
             Search (_ - 0 = _)%Z.
(* Z.sub_0_r: forall n : Z, (n - 0)%Z = n *)
             rewrite <- (Z.sub_0_r a) at 2.
             exact (Z.sub_lt_mono 0 a a 0 lt_0_a lt_0_a). }
           Check (Z.lt_trans (0 - a) a b lt_0_minus_a_0 lt_a_b).
           exact (Z.lt_trans (0 - a) a b lt_0_minus_a_0 lt_a_b).
      * intros [ly _].
        exact ly.
  - destruct (Ztrichotomy b 0) as [lt_b_0 | [eq_b_0 | lt_0_b]].
    + unfold abs.
      destruct (Z.ltb_lt b 0) as [S C].
      rewrite -> (C lt_b_0).
      split.
      * intro lt_a_0_minus_b.
        right.
        exact lt_a_0_minus_b.
      * intros [lt_a_b | lt_a_0_minus_b].
        ** Check (Z.lt_trans a b (0 - b) lt_a_b).
           apply (Z.lt_trans a b (0 - b) lt_a_b).
           Check (Z.lt_trans b 0 (0 - b) lt_b_0). (* : (0 < 0 - b)%Z -> (b < 0 - b)%Z *)
           Search (_ < _ - _)%Z.
           (* Z.lt_add_lt_sub_r: forall n m p : Z, (n + p < m)%Z <-> (n < m - p)%Z *)
           Check (Z.lt_add_lt_sub_r b 0 b).
           destruct (Z.lt_add_lt_sub_r b 0 b) as [foo bar].
           apply foo.
           Search ((_ < _ -> _ < _ -> _ < _)%Z).
           (* Z.add_lt_mono: forall n m p q : Z, (n < m)%Z -> (p < q)%Z -> (n + p < m + q)%Z *)
           Check (Z.add_lt_mono b 0 b 0 lt_b_0 lt_b_0). (* : (b + b < 0 + 0)%Z *)
           rewrite <- (Z.add_0_l 0).
           exact (Z.add_lt_mono b 0 b 0 lt_b_0 lt_b_0).
        ** exact lt_a_0_minus_b.
    + rewrite -> eq_b_0.
      unfold abs.
      rewrite -> (Z.ltb_irrefl 0).
      rewrite -> (Z.sub_diag 0).
      split.
      * intro lt_a_0.
        left.
        exact lt_a_0.
      * intros [lt_a_0 | lt_a_0]; exact lt_a_0.
    + unfold abs.
      destruct (Z.ltb_ge b 0) as [foo bar].
      Check (bar (Z.lt_le_incl 0 b (Z.gt_lt b 0 lt_0_b))).
      rewrite -> (bar (Z.lt_le_incl 0 b (Z.gt_lt b 0 lt_0_b))).
      split.
      * intro lt_a_b.
        left.
        exact lt_a_b.
      * intros [lt_a_b | lt_a_0_minus_b].
        ** exact lt_a_b.
        ** assert (lt_0_minus_b_b :
                     (0 - b < b)%Z).
           { assert (gt_b_0 := lt_0_b).
             clear lt_0_b.
             assert (lt_0_b := Z.gt_lt b 0 gt_b_0).
             rewrite <- (Z.sub_0_r b) at 2.
             exact (Z.sub_lt_mono 0 b b 0 lt_0_b lt_0_b). }
           Check (Z.lt_trans a (0 - b) b lt_a_0_minus_b lt_0_minus_b_b).
           exact (Z.lt_trans a (0 - b) b lt_a_0_minus_b lt_0_minus_b_b).
Qed.

(* ********** *)

Fixpoint zpower (x : Z) (n : nat) : Z :=
  match n with
    O =>
    1%Z
  | S n' =>
    x * zpower x n'
  end.

Lemma fold_unfold_zpower_O :
  forall x : Z,
    zpower x O =
    1%Z.
Proof.
  fold_unfold_tactic zpower.
Qed.

Lemma fold_unfold_zpower_S :
  forall (x : Z)
         (n' : nat),
    zpower x (S n') =
    (x * zpower x n')%Z.
Proof.
  fold_unfold_tactic zpower.
Qed.

(* ********** *)

(* Exercise 07 *)

(* ***** *)

Property about_exponentiating_one :
  forall n : nat,
    (zpower 1 n = 1)%Z.
Proof.
Admitted.

(* ***** *)

Property about_exponentiating_a_product :
  forall (x y : Z)
         (n : nat),
    (zpower (x * y) n = zpower x n * zpower y n)%Z.
Proof.
Admitted.

(* ***** *)

Property about_exponentiating_with_a_sum :
  forall (x : Z)
         (i j : nat),
    (zpower x (i + j) = zpower x i * zpower x j)%Z.
Proof.
Admitted.

(* ***** *)

Property about_exponentiating_with_one :
  forall x : Z,
    (zpower x 1 = x)%Z.
Proof.
Admitted.

(* ***** *)

Property about_exponentiating_with_two :
  forall x : Z,
    (zpower x 2 = x * x)%Z.
Proof.
Admitted.

(* ***** *)

Property about_exponentiating_with_a_product :
  forall (x : Z)
         (y z : nat),
    zpower x (y * z) = zpower (zpower x y) z.
Proof.
Admitted.

(* ***** *)

Property about_the_difference_of_two_squares :
  forall (x y : Z),
    (zpower x 2 - zpower y 2 = (x + y) * (x - y))%Z.
Proof.
Admitted.

Property about_the_difference_of_a_square_and_one :
  forall (x : Z),
    (zpower x 2 - 1 = (x + 1) * (x - 1))%Z.
Proof.
  intro x.
  rewrite -> about_exponentiating_with_two.
  ring.
Qed.

(* ********** *)

(* Exercise 08 *)

Lemma two_times_S :
  forall n : nat,
    2 * S n = S (S (2 * n)).
Proof.
  intro n.
  ring.
Qed.

(* ***** *)

(* Exercise 08a *)

Property about_exponentiating_an_integer_with_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * n + 1) + 1 = q * (x + 1))%Z.
Proof.
  intros x n.
  rewrite -> Nat.add_1_r.
  rewrite -> fold_unfold_zpower_S.
  induction n as [ | n' [q' H_q']].
  - simpl (2 * 0).
    rewrite -> fold_unfold_zpower_O.
    rewrite -> Z.mul_1_r.
    exists 1%Z.
    rewrite -> Z.mul_1_l.
    reflexivity.
  - exists (zpower x (2 * S n') - zpower x (S (2 * n')) + q')%Z.
    rewrite -> Z.mul_add_distr_r.
    rewrite <- H_q'.
    rewrite -> two_times_S.
    repeat (rewrite -> fold_unfold_zpower_S).
    ring.
Qed.

Fixpoint the_pattern_for_Exercise_08a (x : Z) (n : nat) : Z :=
  match n with
    O =>
    1
  | S n' =>
    zpower x (2 * S n') - zpower x (S (2 * n')) + the_pattern_for_Exercise_08a x n'
  end.

Lemma fold_unfold_the_pattern_for_Exercise_08a_O :
  forall x : Z,
    the_pattern_for_Exercise_08a x O =
    1%Z.
Proof.
  fold_unfold_tactic the_pattern_for_Exercise_08a.
Qed.

Lemma fold_unfold_the_pattern_for_Exercise_08a_S :
  forall (x : Z)
         (n' : nat),
    the_pattern_for_Exercise_08a x (S n') =
    (zpower x (2 * S n') - zpower x (S (2 * n')) + the_pattern_for_Exercise_08a x n')%Z.
Proof.
  fold_unfold_tactic the_pattern_for_Exercise_08a.
Qed.

Theorem Exercise_08a:
  forall (x : Z)
         (n : nat),
    (zpower x (2 * n + 1) + 1 = (the_pattern_for_Exercise_08a x n) * (x + 1))%Z.
Proof.
  intros x n.
  rewrite -> Nat.add_1_r.
  rewrite -> fold_unfold_zpower_S.
  induction n as [ | n' IHn'].
  - simpl (2 * 0).
    rewrite -> fold_unfold_zpower_O.
    rewrite -> fold_unfold_the_pattern_for_Exercise_08a_O.
    ring.
  - rewrite -> fold_unfold_the_pattern_for_Exercise_08a_S.
    rewrite -> Z.mul_add_distr_r.
    rewrite <- IHn'.
    rewrite -> two_times_S.
    repeat (rewrite -> fold_unfold_zpower_S).
    ring.
Qed.

(* ***** *)

(* Exercise 08b *)

Property about_exponentiating_an_integer_with_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * n + 1) - 1 = q * (x - 1))%Z.
Proof.
Abort.

(* ********** *)

(* Exercise 09 *)

(* ***** *)

(* Exercise 09a *)

Property about_exponentiating_an_integer_with_the_successor_of_a_multiple_of_four_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (4 * n + 1) + 1 = q * (x + 1))%Z.
Proof.
Abort.

(* ***** *)

(* Exercise 09b *)

Property about_exponentiating_an_integer_with_the_successor_of_a_multiple_of_four_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (4 * n + 1) - 1 = q * (x - 1))%Z.
Proof.
Abort.

(* ********** *)

(* Exercise 10 *)

(* ***** *)

Property about_exponentiating_an_integer_with_zero_times_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (0 * (2 * n + 1)) + 1 = q * (zpower x 0 + 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_one_times_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (1 * (2 * n + 1)) + 1 = q * (zpower x 1 + 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_two_times_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * (2 * n + 1)) + 1 = q * (zpower x 2 + 1))%Z.
Proof.
Abort.

(* ***** *)

Lemma three_times_S :
  forall n : nat,
    3 * S n = S (S (S (3 * n))).
Proof.
  intro n.
  ring.
Qed.

Property about_exponentiating_an_integer_with_three_times_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (3 * (2 * n + 1)) + 1 = q * (zpower x 3 + 1))%Z.
Proof.
Abort.

(* ***** *)

Lemma eight_times_S :
  forall n : nat,
    8 * S n = S (S (S (S (S (S (S (S (8 * n)))))))).
Proof.
  intro n.
  ring.
Qed.

Property about_exponentiating_an_integer_with_four_times_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (8 * n + 4) + 1 = q * (zpower x 4 + 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_the_multiple_of_an_odd_natural_number_and_then_adding_one :
  forall (x : Z)
         (n k : nat),
  exists q : Z,
    (zpower x (k * (2 * n + 1)) + 1 = q * (zpower x k + 1))%Z.
Proof.
Abort.

(* ********** *)

(* Exercise 11 *)

(* ***** *)

Property about_exponentiating_an_integer_with_zero_times_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (0 * (2 * n + 1)) - 1 = q * (zpower x 0 - 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_one_times_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (1 * (2 * n + 1)) - 1 = q * (zpower x 1 - 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_two_times_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * (2 * n + 1)) - 1 = q * (zpower x 2 - 1))%Z.
Proof.
Abort.

Property about_exponentiating_an_integer_with_three_times_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (3 * (2 * n + 1)) - 1 = q * (zpower x 3 - 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_four_times_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (8 * n + 4) - 1 = q * (zpower x 4 - 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_the_multiple_of_an_odd_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n k : nat),
  exists q : Z,
    (zpower x (k * (2 * n + 1)) - 1 = q * (zpower x k - 1))%Z.
Proof.
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_an_even_natural_number_and_then_subtracting_one_alt :
  forall (x : Z)
         (n : nat),
  exists q : Z,
    (zpower x (2 * n) - 1 = q * (zpower x 2 - 1))%Z.
Proof. 
Abort.

(* ***** *)

Property about_exponentiating_with_four :
  forall x : Z,
    (zpower x 4 = x * x * x * x)%Z.
Proof.
  intro x.
  rewrite ->4 fold_unfold_zpower_S.
  rewrite -> fold_unfold_zpower_O.
  ring.
Qed.

Property about_exponentiating_an_integer_with_four_times_a_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
    exists q : Z,
      (zpower x (4 * n) - 1 = q * (zpower x 4 - 1))%Z.
Proof. 
Abort.

(* ***** *)

Lemma six_times_S :
  forall n : nat,
    6 * S n = S (S (S (S (S (S (6 * n)))))).
Proof.
  intro n.
  ring.
Qed.

Property about_exponentiating_with_six :
  forall x : Z,
    (zpower x 6 = x * x * x * x * x * x)%Z.
Proof.
  intro x.
  rewrite ->6 fold_unfold_zpower_S.
  rewrite -> fold_unfold_zpower_O.
  ring.
Qed.

Property about_exponentiating_an_integer_with_six_times_a_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n : nat),
    exists q : Z,
      (zpower x (6 * n) - 1 = q * (zpower x 6 - 1))%Z.
Proof. 
Abort.

(* ***** *)

Property about_exponentiating_an_integer_with_an_even_multiple_of_a_natural_number_and_then_subtracting_one :
  forall (x : Z)
         (n k : nat),
    exists q : Z,
      (zpower x (2 * k * n) - 1 = q * (zpower x (2 * k) - 1))%Z.
Proof. 
Abort.

(* ********** *)

(* Exercise 13 *)

Property about_exponentiating_an_integer_with_a_product_of_natural_numbers_and_then_subtracting_one :
  forall (x : Z)
         (m n : nat),
    exists q : Z,
      (zpower x (m * n) - 1 = q * (zpower x m - 1))%Z.
Proof.
Abort.

(* ********** *)

(* end of week-10_integers.v *)