proposition: Lemma isarchnat_pos : ∏ x : nat, ∃ n : nat, n + x > 0.
proof: Proof. intros n. apply hinhpr. now exists 1%nat. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations