Lemma isarchnat_pos : ∏ x : nat, ∃ n : nat, n + x > 0. Proof. intros n. apply hinhpr. now exists 1%nat. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.