(* This should be in the Coq library *)
Require Import Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith.

Lemma N_to_Z_to_nat: forall (a: N), Z.to_nat (Z.of_N a) = N.to_nat a.
Proof.
(* Goal: forall n m : nat, @eq Z (Z.of_nat (Nat.pow n m)) (Z.pow (Z.of_nat n) (Z.of_nat m)) *)
  intros. rewrite <- (N2Z.id a) at 2.
(* Goal: @eq nat (Z.to_nat (Z.of_N a)) (N.to_nat (Z.to_N (Z.of_N a))) *)
  rewrite Z_N_nat. reflexivity.
Qed.

Module N2Nat.

  Lemma inj_mod: forall (a b: N),
      (b <> 0)%N ->
      N.to_nat (a mod b)%N = (N.to_nat a) mod (N.to_nat b).
  Proof.
(* Goal: forall n m : nat, @eq Z (Z.of_nat (Nat.pow n m)) (Z.pow (Z.of_nat n) (Z.of_nat m)) *)
    intros.
(* Goal: @eq nat (N.to_nat (N.modulo a b)) (Nat.modulo (N.to_nat a) (N.to_nat b)) *)
    rewrite <-? N_to_Z_to_nat.
(* Goal: @eq nat (Z.to_nat (Z.of_N (N.modulo a b))) (Nat.modulo (Z.to_nat (Z.of_N a)) (Z.to_nat (Z.of_N b))) *)
    rewrite N2Z.inj_mod by assumption.
(* Goal: @eq nat (Z.to_nat (Z.modulo (Z.of_N a) (Z.of_N b))) (Nat.modulo (Z.to_nat (Z.of_N a)) (Z.to_nat (Z.of_N b))) *)
    apply Nat2Z.inj.
(* Goal: @eq Z (Z.of_nat (Z.to_nat (Z.modulo (Z.of_N a) (Z.of_N b)))) (Z.of_nat (Nat.modulo (Z.to_nat (Z.of_N a)) (Z.to_nat (Z.of_N b)))) *)
    rewrite Zdiv.mod_Zmod.
    - rewrite? Z2Nat.id; try apply N2Z.is_nonneg.
(* Goal: @eq Z (Z.of_nat (Nat.pow n (S m))) (Z.of_nat (Init.Nat.mul n (Nat.pow n m))) *)
      + reflexivity.
      + pose proof (Z.mod_pos_bound (Z.of_N a) (Z.of_N b)) as Q.
(* Goal: Z.le Z0 (Z.modulo (Z.of_N a) (Z.of_N b)) *)
        destruct Q as [Q _].
        * destruct b; try contradiction. simpl. constructor.
        * exact Q.
    - destruct b; try contradiction. simpl.
(* Goal: not (@eq nat (Pos.to_nat p) O) *)
      pose proof (Pos2Nat.is_pos p) as Q. omega.
  Qed.

End N2Nat.

Module Nat2Z.

  Lemma inj_pow: forall n m : nat,
      Z.of_nat (n ^ m) = (Z.of_nat n ^ Z.of_nat m)%Z.
  Proof.
(* Goal: forall n m : nat, @eq Z (Z.of_nat (Nat.pow n m)) (Z.pow (Z.of_nat n) (Z.of_nat m)) *)
    intros. induction m.
(* Goal: @eq Z (Z.of_nat (Nat.pow n (S m))) (Z.of_nat (Init.Nat.mul n (Nat.pow n m))) *)
    - reflexivity.
    - rewrite Nat2Z.inj_succ.
(* Goal: @eq Z (Z.of_nat (Nat.pow n (S m))) (Z.pow (Z.of_nat n) (Z.succ (Z.of_nat m))) *)
      rewrite Z.pow_succ_r by (apply Nat2Z.is_nonneg).
      rewrite <- IHm.
      rewrite <- Nat2Z.inj_mul.
(* Goal: @eq Z (Z.of_nat (Nat.pow n (S m))) (Z.of_nat (Init.Nat.mul n (Nat.pow n m))) *)
      reflexivity.
  Qed.

End Nat2Z.

Module Z2Nat.

  Lemma inj_pow: forall n m : Z,
      (0 <= n)%Z ->
      (0 <= m)%Z ->
      Z.to_nat (n ^ m) = Z.to_nat n ^ Z.to_nat m.
  Proof.
(* Goal: forall n m : nat, @eq Z (Z.of_nat (Nat.pow n m)) (Z.pow (Z.of_nat n) (Z.of_nat m)) *)
    intros.
    pose proof (Nat2Z.inj_pow (Z.to_nat n) (Z.to_nat m)) as P.
    rewrite? Z2Nat.id in P by assumption.
    rewrite <- P.
    apply Nat2Z.id.
  Qed.

End Z2Nat.
