Definition weqdnicoprod_invmap {n : nat} (j : ⟦S n⟧ ) : ⟦n⟧ ⨿ unit <- ⟦S n⟧. Proof. intros i. induction (isdeceqstn (S n) i j) as [eq|ne]. - exact (ii2 tt). - apply ii1. induction i as [i I]. induction j as [j J]. choose (i < j)%dnat a a. + exists i. exact (natltltSlt _ _ _ a J). + exists (i - 1). induction (natlehchoice _ _ (negnatgthtoleh a)) as [b|b]. * induction (natlehchoice4 _ _ I) as [c|c]. -- apply (natlehlthtrans (i - 1) i n). ++ apply natminuslehn. ++ exact c. -- induction c. apply natminuslthn. ++ apply (natlehlthtrans _ j _). ** apply natleh0n. ** exact b. ++ apply natlthnsn. * induction b. induction (ne (@subtypePath_prop _ _ (make_stn _ j I) (make_stn _ j J) (idpath j))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.