proposition: Lemma inaccessible_weak_strong x: inaccessible_w x -> inaccessible x.
proof: Proof. move => h; split => // t th. move: h => [[pa pb] [n [on _ ln xv]]]. case: (finite_or_infinite (proj31_1 th)) => it. apply:(clt_fin_inf) => //. apply /NatP; apply: NS_pow; apply /NatP;fprops. move: th; rewrite - (gch it). move: (ord_index_pr1 it) => [om <-]; rewrite (cnextE om) xv => le1. move: (aleph_ltc_lt om on le1) => mn. apply: aleph_lt_ltc; apply /oltP0; split;fprops. apply: ln; apply /oltP => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)