proposition: Lemma consec_pow_pr3 r f: order r -> consec_list r f -> (domain f) <=cc (substrate r).
proof: Proof. move => ha hb; rewrite (consec_pow_pr2 ha hb). move:(hb) =>[qa qb qc qd]. apply: sub_smaller => t /(range_gP qa) [x xdf ->]; apply: qc. apply/(range_gP qa); ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)