proposition: Lemma consec_pow_pr8 r x (E := substrate r) : total_order r -> finite_set E -> inc x E -> consec_pow r x = cardinal E.
proof: Proof. move => ha hb hc. move: (finite_ordered_interval1 ha hb) => [f /proj1]. move/card_finite_setP:hb. rewrite -/E; set n := cardinal _ => nN is1. rewrite (consec_pow_pr7 is1 hc) (consec_pow_pr5 nN) //. apply/(NltP nN); rewrite - (NintE nN) -(proj2 (Nintco_wor n)). move:(is1) => [_ _ [[[ff _] _] sf <-] _]; Wtac; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)