proposition: Lemma consec_pow_pr2 r f: order r -> consec_list r f -> (domain f) =c (range f).
proof: Proof. move => or [ha hb _ hc]. pose g := Lf (Vg f) (domain f) (range f). have <- : source g = domain f by rewrite /g;aw. have <- : target g = range f by rewrite /g;aw. have ax: lf_axiom (Vg f) (domain f) (range f). by move => x xdf; apply/(range_gP ha); ex_tac. have rx y:inc y (range f) -> exists2 x, inc x (domain f) & y = Vg f x. by move/(range_gP ha). have fm i j: i <c j -> j <c (domain f) -> glt r (Vg f i) (Vg f j). move => qa qb; move: (NS_lt_nat qb hb) => jN; move: j jN qa qb. apply: Nat_induction; first by move/clt0. move => j jN Hrec lij ljd; move: (proj1 (hc j jN ljd)) => lt1. move/(cltSleP jN): lij; case/cle_eqVlt => cij; first by rewrite cij. exact (lt_lt_trans or (Hrec cij (cle_ltT (cleS jN) ljd)) lt1). apply: card_bijection; apply: lf_bijective => // u v udx vdx df. move/(NltP hb): udx => us; move/(NltP hb): vdx => vs. case: (NleT_ell (NS_lt_nat us hb)(NS_lt_nat vs hb)) => // ll. by case:(proj2(fm _ _ ll vs)). by case:(proj2(fm _ _ ll us)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)