proposition: Lemma inaccessible_pr5 x: \2c <c x -> (forall f, cprod_of_small f x -> cprod f <c x) -> (x = omega0 \/ inaccessible x).
proof: Proof. move=> h1 h2. case: (inaccessible_pr4 h1 h2) => lx; first by left. move: (inaccessible_pr3 h1 h2) => [pa pb]. right; split; last by move => t tx; apply: pb. split => //; split => //. have H:=(cofinality_card pa). rewrite H;ex_middle cs. have pe: \cf x <c x by split => //; exact (cofinality_small pa). move: (cofinality_c_pr3 pa) =>[f [[qa qb] df sf etc]]. have cff: cardinal_fam f by move => t /qb /proj31_1. have: cprod_of_small f x by split => //; rewrite df H. move /h2 => l2. by move: (compare_sum_prod1 qa etc); rewrite sf => /(cltNge l2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)