proposition: Lemma inaccessible_pr7 x y: inaccessible x -> y <> \0c -> y <c x -> x ^c y = x.
proof: Proof. move => [[[icx cfx] pb] pc] pd pe. rewrite (cofinality_card icx) in cfx. rewrite - cfx in pe. move: (icx) => [cx _]. rewrite (infinite_power7 icx pe pd) /csumb. set f := Lg _ _. have snz: csum f <> \0c. suff: \1c <=c csum f by move/cge1P =>[_ /nesym]. have zi: inc \1c (cardinals_lt x). by apply /(cardinals_ltP cx); apply: infinite_gt1. have zi1: inc \1c (domain f) by rewrite /f; aw. move: CS1. have <-: Vg f \1c = \1c by rewrite/f LgV// cpow1x. by move => cc;apply:(csum_increasing6 cc zi1). rewrite cprodC; apply: (cprod_inf) => //. have dx:card_dominant x. by apply: card_dominant_pr1 => //; apply infinite_nz. rewrite cfx in pe. have pf: csum_of_small1 x f. rewrite /f;split; fprops; hnf; aw; move => i idf; rewrite LgV//. by move: idf => /(cardinals_ltP cx) => idf;apply (proj2 dx). move: (csum_of_small_b2 pf) => le1. have df: cardinal (domain f) <=c x. rewrite Lgd. by case: (infinite_power7d cx (infinite_nz icx)). by move: (cprod_inf1 df icx);rewrite cprod2cr; apply: cleT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)