Lemma weqcutforstn ( n n' : nat ) : ⟦S n⟧ ≃ ⟦S n'⟧ -> ⟦n⟧ ≃ ⟦n'⟧. Proof. intros w. assert ( k := @lastelement n ). intermediate_weq (stn_compl k). - apply weqdnicompl. - intermediate_weq (stn_compl (w k)). + apply weqoncompl_ne. + apply invweq, weqdnicompl. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.