Lemma nattorig_nat : ∏ n : nat, nattorig (X := natcommrig) n = n. Proof. induction n as [|n IHn]. reflexivity. rewrite nattorigS, IHn. reflexivity. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.