proposition: Lemma weqcutforstn ( n n' : nat ) : ⟦S n⟧ ≃ ⟦S n'⟧ -> ⟦n⟧ ≃ ⟦n'⟧.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions