N_le_zero@{} (n : N) (H : n <= zero) : n = zero. Proof. destruct H as [k H]. apply pr1_path in H. apply ((equiv_path_graph _ _)^-1), pr1 in H. pose proof ((fun x => H (inr x)) : (vert n.1) -> Empty) as f. apply path_N, equiv_path_graph. srefine ((Build_Equiv _ _ f _);_); cbn. intros x y; destruct (f x). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.