Lemma weqfromcoprodofstn_eq2 (n m : nat) : ∏ y : ⟦n+m⟧, weqfromcoprodofstn_map n m (weqfromcoprodofstn_invmap n m y) = y. Proof. intros x. unfold weqfromcoprodofstn_map, weqfromcoprodofstn_invmap. unfold coprod_rect. induction (natlthorgeh x n) as [H | H]. - apply isinjstntonat. apply idpath. - induction (natchoice0 m) as [H1 | H1]. + apply fromempty. induction H1. induction (! (natplusr0 n)). use (natlthtonegnatgeh x n (stnlt x) H). + apply isinjstntonat. cbn. rewrite natpluscomm. apply minusplusnmm. apply H. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.