blob: d6dd49a4182bd4e135c849f7b1d6734c36521ede (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
Local Open Scope Z_scope.
Module Z2Nat.
Definition inj_nonpos n : n <= 0 -> Z.to_nat n = 0%nat.
Proof.
destruct n; try reflexivity; lia.
Qed.
End Z2Nat.
|