proposition: Lemma finite_enumeration_stage (n : nat) : IsEmbedding (er n) + { n : nat & { k : nat & e n = e (n + k).+1 }}.
proof: Proof. induction n as [|n [IH|IH]]. - left. intros x. apply hprop_inhabited_contr; intros [[] _]. - destruct (detachable_image_finite (er n) (er n.+1 (inr tt))) as [[k p]|ne]. + right. exists (nat_fin n k). exists (nat_fin_compl n k). rewrite nat_fin_compl_compl. exact p. + left. intros x. apply hprop_allpath. intros k l. apply path_sigma_hprop. destruct k as [[k|[]] p], l as [[l|[]] q]; simpl. * apply isinj_embedding in IH. apply ap. apply IH. unfold er in p, q. simpl in p, q. exact (p @ q^). * refine (Empty_rec (ne _)). exists k. exact (p @ q^). * refine (Empty_rec (ne _)). exists l. exact (q @ p^). * reflexivity. - right; exact IH. Defined.
imports: Basics Types HSet Spaces.Nat.Core HFiber Factorization Truncations Colimits.Quotient Projective Fin