Definition coprod_stn_assoc (l m n : nat) : ( eqweqmap (maponpaths stn (natplusassoc l m n)) ∘ weqfromcoprodofstn (l+m) n ∘ weqcoprodf (weqfromcoprodofstn l m) (idweq _) ~ weqfromcoprodofstn l (m+n) ∘ weqcoprodf (idweq _) (weqfromcoprodofstn m n) ∘ weqcoprodasstor _ _ _ ) %weq. Proof. intros. intros abc. simpl. apply (invmaponpathsincl pr1). apply isinclstntonat. rewrite pr1_eqweqmap_stn. induction abc as [[a|b]|c]. - simpl. apply idpath. - simpl. apply idpath. - simpl. apply natplusassoc. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.