proposition: Lemma consec_pow_pr4 n i : natp n -> i <c n -> consec_list_for (Nint_co n) (identity_g n) i.
proof: Proof. move => nN /(NltP nN)lin. have ha:= (identity_fgraph n). have hb:= (identity_d n). split; last first. by apply/(range_gP ha); rewrite hb; ex_tac; rewrite identity_ev. move: (Nintco_wor n) =>[[or _] sr]. split; rewrite ?hb => //. by rewrite sr (NintE nN) identity_r. move => j jN ljn. move: (cltS jN) => [qa qb]. have jn: inc j n. apply/(NltP nN); apply: (cle_ltT qa ljn). have sjn: inc (csucc j) n by apply/(NltP nN). split. rewrite (identity_ev jn) (identity_ev sjn). split; [ by apply /(Nintco_gleP nN) | exact ]. rewrite sr (NintE nN) => z zn [qc qd]. case: qc; case: qd; rewrite (identity_ev jn) (identity_ev sjn). move=> /(Nintco_gleP nN) [ eqa _] eqb /(Nintco_gleP nN) [eqc _]; case. by apply: cleA => //;move/(cltSleP jN): (conj eqa eqb). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)