N_lt_zero@{} (n : N) : ~(n < zero). Proof. unfold N_lt; intros [k H]. apply pr1_path, (equiv_path_graph _ _)^-1, pr1 in H. exact (H (inl (inr tt))). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.