Lemma isarchnat : isarchrig (X := natcommrig) natgth. Proof. repeat split. - intros y1 y2 Hy. generalize (isarchnat_diff y1 y2 Hy). apply hinhfun. intros n. exists (pr1 n). rewrite nattorig_nat. exact (pr2 n). - intros n. generalize (isarchnat_gth n). apply hinhfun. intros n'. exists (pr1 n'). rewrite nattorig_nat. exact (pr2 n'). - intros n. generalize (isarchnat_pos n). apply hinhfun. intros n'. exists (pr1 n'). rewrite nattorig_nat. exact (pr2 n'). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.