proposition: Lemma isembedding_fsucc@{} {n : nat} : IsEmbedding (@fsucc n).
proof: Proof. apply isembedding_isinj_hset. simple_induction n n IHn. - intro i. elim i. - intros [] []; intro p. + f_ap. apply IHn. eapply path_sum_inl. exact p. + destruct u. elim (inl_ne_inr _ _ p). + destruct u. elim (inr_ne_inl _ _ p). + destruct u, u0; reflexivity. Defined.
imports: Basics Types HSet Spaces.Nat.Core Equiv.PathSplit