proposition: Lemma isarchnat_diff : ∏ (y1 y2 : nat), y1 > y2 → ∃ n : nat, n * y1 > 1 + n * y2.
proof: Proof. intros y1 y2 Hy. apply natlthchoice2 in Hy. induction Hy as [Hy | <-]. - apply hinhpr. exists 1%nat. exact Hy. - apply hinhpr. exists 2%nat. rewrite !multsnm ; simpl. rewrite natplusr0. apply natgthandplusl, natgthsnn. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations