proposition: Lemma weqfromcoprodofstn_eq1 (n m : nat) : ∏ x : ⟦n⟧ ⨿ ⟦m⟧, weqfromcoprodofstn_invmap n m (weqfromcoprodofstn_map n m x) = x.
proof: Proof. intros x. unfold weqfromcoprodofstn_map, weqfromcoprodofstn_invmap. unfold coprod_rect. induction x as [x | x]. - induction (natlthorgeh (stn_left n m x) n) as [H | H]. + apply maponpaths. apply isinjstntonat. apply idpath. + apply fromempty. apply (natlthtonegnatgeh x n (stnlt x) H). - induction (natlthorgeh (stn_right n m x) n) as [H | H]. + apply fromempty. set (tmp := natlehlthtrans n (n + x) n (natlehnplusnm n x) H). use (isirrefl_natneq n (natlthtoneq _ _ tmp)). + apply maponpaths. apply isinjstntonat. cbn. rewrite natpluscomm. apply plusminusnmm. Qed.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions