Lemma isarchnat_gth : ∏ x : nat, ∃ n : nat, n > x. Proof. intros n. apply hinhpr. exists (S n). now apply natgthsnn. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.