proposition: Lemma cpow_less_ec_pr2 x y a: cpow_less_ec_prop x y a -> \2c <=c x -> forall b, a<=c b -> b <c y -> x ^<c y = x ^c b.
proof: Proof. move =>[ay h] x2 b le1 le2. have xnz := (card_ge2_nz x2). apply: cleA; last by apply: cpow_less_pr2. have cy:= proj32_1 le2. apply: card_ub_sup; first fprops. move => i /funI_P [z /(cardinals_ltP cy) lt1 ->]. case: (cleT_ee (proj31 le1) (proj31_1 lt1)) => az. rewrite - (h _ az lt1) (h _ le1 le2). apply: (cleR); fprops. exact (cpow_Meqle xnz (cleT az le1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)