proposition: Lemma isarchnat_gth : ∏ x : nat, ∃ n : nat, n > x.
proof: Proof. intros n. apply hinhpr. exists (S n). now apply natgthsnn. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations