proposition: Lemma cpow_less_pr9 x (y := cnext x): infinite_c x -> ( y ^<c y = \2c ^c x /\ \2c ^<c y = \2c ^c x).
proof: Proof. move => icx; move: (icx) => [cx _]. have sp:= (cle_ltT(cle0x cx) (cnext_pr2 cx)). rewrite (cpow_less_pr4 clt_02 icx) (cpow_less_pr4 sp icx). by rewrite (infinite_power1_c icx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)