proposition: Lemma Exercise_6_20c2: (forall a, regular_cardinal a -> (forall m, \0c <c m -> m <c a -> a ^c m = a)) -> GenContHypothesis.
proof: Proof. move => h. move => t ict; move: (ict) => [ct _]. move: (ord_index_pr1 ict)=> [on tv]. move: (regular_initial_successor on). rewrite - (cnextE on) tv => rs. move: (h _ rs _ (clt_fin_inf finite_0 ict) (cnext_pr2 ct)). move => le1. apply: cleA; first by apply: (cnext_pr3 ct). have pa: \2c <=c cnext t. rewrite -tv (cnextE on). apply: (cle_fin_inf finite_2 (CIS_aleph (OS_succ on))). by rewrite -le1; apply: (cpow_Mleeq _ pa card2_nz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)