proposition: Lemma consec_pow_pr5 n i : natp n -> i <c n -> consec_pow (Nint_co n) i = n.
proof: Proof. move => ha hb. move: (consec_pow_pr4 ha hb) => H. rewrite /consec_pow; set T := fun_image _ _. move: (Nintco_wor n) =>[[or _] sr]. have hc: inc (identity_g n) (consec_lists_for (Nint_co n) i). by apply/ consec_pow_pr0. have hd t: inc t T -> t <=c n. move=> /funI_P [u /consec_pow_pr0 /proj1 ua ->]. move: (consec_pow_pr3 or ua); rewrite sr (NintE ha). rewrite (card_card (CS_nat (proj42 ua))). by rewrite (card_card (CS_nat ha)). apply: (cleA (card_ub_sup (CS_nat ha) hd)). apply: card_sup_ub; first by move => t /hd/proj31. by apply/funI_P; ex_tac; rewrite identity_d. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)