Library Flocq.Pff.Nat2Z_8_12

Require Import ZArith.

Module Nat2Z.

Notation inj_lt := Nat2Z.inj_lt.
Notation inj_le := Nat2Z.inj_le.
Notation inj := Nat2Z.inj.

Lemma inj_div n m : Z.of_nat (n / m) = (Z.of_nat n / Z.of_nat m)%Z.

End Nat2Z.