proposition: Lemma cpow_less_ec_pr3 x y a: cpow_less_ec_prop x y a -> \2c <=c x -> singular_cardinal y -> (x ^<c y = x ^c a /\ x ^<c y = x ^c y).
proof: Proof. move => h x2 [icy sy]; move: (h) => [ay h0]. have h1:= (cpow_less_ec_pr2 h x2). have ca:= (proj31_1 ay). rewrite (h1 _ (cleR ca) ay). split; first by exact. have cg:= (cofinality_small icy). have [c [ac cf cx]]: exists c, [/\ a <=c c, \cf y <=c c &c <c y]. have cx:= proj31 cg. case: (cleT_ee ca cx) => cp; last by exists a; split;fprops. exists (\cf y); split => //; split; fprops. have coi:=(cofinality_infinite_cardinal icy). have cnz:=(infinite_nz coi). have icc:= (cle_inf_inf coi cf). rewrite (cpow_less_pr6 icy x2) (h1 _ ac cx) - cpow_pow. by rewrite (cprod_inf cf icc cnz) (h0 _ ac cx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)