proposition: Lemma nat_of_Z_nonneg (x : Z) : 0 <= x -> Z_of_nat (nat_of_Z x) = x.
proof: Proof. destruct x; simpl. reflexivity. intros. apply Z_of_nat_of_P. now intros []. Qed.
imports: Coq.ZArith.ZArith CoRN.stdlib_omissions.P Lia