proposition: Lemma beth_gch: GenContHypothesis <-> beth =1o \aleph.
proof: Proof. split; last first. move => h x icx. move: (ord_index_pr1 icx) => [oy <-]. by rewrite (cnextE oy) - (h _ oy) - (beth_succ oy) (h _ (OS_succ oy)). move =>h x ox. case:(least_ordinal6 (fun z => beth z = \aleph z) ox) => //. set y := least_ordinal _ _; move =>[pa pb];case. case: (ordinal_limA pa). - by move => ->; rewrite aleph0E beth0. - move=> [u ou u1]. rewrite u1 (beth_succ ou) - (cnextE ou) (h _ (CIS_aleph ou)). rewrite pb // u1; fprops. move=> lt. rewrite (proj2 beth_normal _ lt) (proj2 aleph_normal _ lt). by apply: ord_sup_2funI => s st; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)