zero_neq_succ@{} (n : N) : zero <> succ n. Proof. intros p; apply pr1_path in p; refine (graph_zero_neq_succ p). Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.