Definition weqdnicompl {n : nat} (i: ⟦S n⟧ ): ⟦n⟧ ≃ stn_compl i. Proof. intros. set (w := weqdicompl (stntonat _ i)). assert (eq : ∏ j, j < n <-> pr1 (w j) < S n). { simpl in w. intros j. unfold w. change (pr1 ((weqdicompl i) j)) with (di (stntonat _ i) j). unfold di. induction (natlthorgeh j i) as [lt|ge]. - split. + apply natlthtolths. + intros _. exact (natlehlthtrans (S j) i (S n) lt (pr2 i)). - split; exact (idfun _). } refine (_ ∘ (weq_subtypes w (λ j, j < n) (λ j, pr1 j < S n) eq))%weq. use weqtotal2comm12. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.