Lemma isarchnat_diff : ∏ (y1 y2 : nat), y1 > y2 → ∃ n : nat, n * y1 > 1 + n * y2. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.