Require Import Bool.
Require Import Setoid.
Require Import Coq.Logic.Eqdep_dec.
Require Import ZArith Znumtheory.
Require Import Ring.
Require Import Field.
Require Import Specif.
Require Import ProofIrrelevance.
Require Import Coq.PArith.Pnat.
Require Import Coq.ZArith.Znat.
Require Import ArithRing.
Require Import Psatz.
Require Import Recdef.
Require Import Div2.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.ZArith.Znat.

Lemma mod_irr : forall a : Z,
  0 <= a ->
  Z.to_nat (a mod Q) =  Nat.modulo (Z.to_nat a) (Z.to_nat Q).
Proof.
  intros a Ha.
  assert (Ht : exists (k r : Z), k >= 0 /\ 0 <= r < Q /\ a = r + k * Q).
  assert (Q <> 0). unfold Q.  lia.
  pose proof (Z.div_mod a Q H).
  exists (a / Q), (a mod Q).
  split. unfold Q.
  apply Z_div_ge0. lia.  lia.
  split. apply Z.mod_pos_bound. unfold Q. lia.
  lia.
  destruct Ht as [k [r [Ht1 [Ht2 Ht3]]]].
  rewrite Ht3.
  rewrite Z_mod_plus_full.
  rewrite Z.mod_small; swap 1 2.
  assumption.
  rewrite Z2Nat.inj_add.
  rewrite Z2Nat.inj_mul.
  rewrite Nat.mod_add.
  rewrite Nat.mod_small. auto.
  apply Z2Nat.inj_lt; try lia.
  subst. cbn. lia.
  lia.  lia.  lia.  unfold Q. lia.
Qed.



I see a very similar lemma for nat

mod_Zmod
     : forall n m : nat, m <> 0%nat -> Z.of_nat (n mod m) = Z.of_nat n mod Z.of_nat m

and I am looking for very similar thing in Z.