proposition: Lemma le_Zle_to_nat (n : nat) (z : Z) : (Z.to_nat z <= n)%nat <-> z <= Z.of_nat n.
proof: Proof. pose proof (Nat.le_0_l n). pose proof (Zle_0_nat n). destruct (Z.neg_nonneg_cases z). + rewrite Zto_nat_nonpos by now apply Z.lt_le_incl. split; auto with zarith. + split; intro A. - apply inj_le in A. rewrite Z2Nat.id in A; trivial. - apply Z2Nat.inj_le in A; trivial. rewrite Nat2Z.id in A; trivial. Qed.
imports: Coq.ZArith.ZArith CoRN.stdlib_omissions.P Lia