Definition nelstructoncompl {X : UU} {n : nat} (x : X) : nelstruct (S n) X -> nelstruct n (compl X x). Proof. intros sx. refine (invweq (weqoncompl (invweq sx) x) ∘ _ ∘ weqdnicompl (invweq sx x))%weq. apply compl_weq_compl_ne. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.