proposition: Lemma inaccessible_pr6 x: inaccessible x -> (forall f, cprod_of_small f x -> cprod f <c x).
proof: Proof. move => [[[cx rx] pb] pc] f [pe pf pg]. set z := domain f in pg. set f' := (Lg z (Vg f)). have df' : domain f' = z by rewrite /f'; aw. have pa: csum_of_small1 x f'. by rewrite /f';split; fprops;hnf; aw => i idf; rewrite LgV//; apply: pf. have cff: cardinal_fam f' by move => t /(proj2 pa) /proj31_1. set su := csum f'. have sux: su <=c x. move: (csum_of_small_b2 pa); rewrite df' => qb. exact: (cleT qb (cprod_inf1 (proj1 pg) cx)). case: (equal_or_not su x) => sux1. have: cofinality_c x <=o z. move: (cofinality_c_rw (infinite_ge2 cx)) => [_ _ cfxp]. by apply: (cfxp _ (proj1 (proj31_1 pg))); exists f'. by move: (oclt pg); rewrite rx => qa /(oltNge qa). have dx:card_dominant x. apply: card_dominant_pr1 => //; [ exact: (proj32 sux) | by apply infinite_nz]. apply: cle_ltT ((proj2 dx) _ _ (conj sux sux1) pg). rewrite - cprod_of_same; apply cprod_increasing;rewrite /cst_graph; aw; trivial. move => i idf; rewrite LgV//. have udf': inc i (domain f') by ue. move: (csum_increasing6 (cff _ udf') udf'); rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)