Definition sni {n : nat} ( i : ⟦n⟧ ) : ⟦n⟧ <- ⟦S n⟧. Proof. intros j. exists (si i j). unfold si. induction (natlthorgeh i j) as [lt|ge]. - induction j as [j J]. induction i as [i I]. simpl. induction j as [|j _]. + contradicts (negnatlthn0 i) lt. + change (S j - 1 < n). change (S j) with (1 + j). rewrite natpluscomm. rewrite plusminusnmm. exact J. - induction i as [i I]. exact (natlehlthtrans _ _ _ ge I). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.