proposition: Lemma IFE_consec_chain4 x : inc x IFSE -> consec_pow IFS_order x = IFS_pow x.
proof: Proof. move => xE. have lt1: IFS_pow x <=c consec_pow IFS_order x. apply: card_sup_ub. by move => t /funI_P [a /consec_pow_pr0 /proj1/proj42/CS_nat aa ->]. by apply/funI_P; move: (IFE_consec_chain2 xE) =>[f qa qb]; ex_tac. apply: (cleA _ lt1). apply: (card_ub_sup (proj31 lt1)). move => i /funI_P [f ff ->]. by apply:IFE_consec_chain3. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)