Theorem weqweqstnsn ( n : nat ) : (⟦S n⟧ ≃ ⟦S n⟧) ≃ ⟦S n⟧ × ( ⟦n⟧ ≃ ⟦n⟧ ). Proof. assert ( l := @lastelement n ). intermediate_weq ( isolated (⟦S n⟧) × (compl _ l ≃ compl _ l) ). { apply weqcutonweq. intro i. apply isdeceqstn. } apply weqdirprodf. - apply weqisolatedstntostn. - apply weqweq. apply invweq. intermediate_weq (compl_ne (⟦S n⟧) l (stnneq l)). + apply weqdnicompl. + apply compl_weq_compl_ne. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.