Definition weqdnicoprod_provisional (n : nat) (j : ⟦S n⟧) : ⟦n⟧ ⨿ unit ≃ ⟦S n⟧. Proof. intros. apply (weqcomp (weqcoprodf (weqdnicompl j) (idweq unit)) (weqrecompl_ne (⟦S n⟧) j (isdeceqstn (S n) j) (stnneq j))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.