contr_le_zero@{} : Contr {n:N & n <= zero}. Proof. apply (Build_Contr _ (exist (fun n => n <= zero) zero (N_zero_le zero))). intros [n H]. apply path_sigma_hprop. exact (N_le_zero n H)^. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.