proposition: Lemma consec_pow_pr9 r (E := substrate r) : order r -> finite_set E -> (exists2 x, inc x E & consec_pow r x = cardinal E) -> total_order r.
proof: Proof. move => or fse [x xE ]. rewrite /consec_pow; set T := fun_image _ _ => h. move/card_finite_setP: (fse); set n := cardinal E => nN. have hd t: inc t T -> t <=c n. move=> /funI_P [u /consec_pow_pr0 /proj1 ua ->]. move: (consec_pow_pr3 or ua). by rewrite (card_card (CS_nat (proj42 ua))). case:(all_exists_dichot1 (fun z => z <c n) T) => hyp. case: (equal_or_not n \0c) => ez. move: (card_nonempty ez) => Ez. by split => //u v; rewrite -/E Ez => /in_set0. move: (cpred_pr nN ez); set p:= cpred n; move => [pN pv]. have he t: inc t T -> t <=c p. by move => tT; apply/(cltSleP pN); rewrite - pv; apply: hyp. move: (card_ub_sup (CS_nat pN) he); rewrite h -/n => /cleNgt; case. by move: (cltS pN); rewrite pv. move: hyp => [m ma mb]. have: inc n T. case: (equal_or_not m n); first by move <-. by move => h1;case: mb; split => //; apply: hd. move/funI_P =>[f /consec_pow_pr0/proj1 qa qb]. move: (qa) =>[ha hb hc he]; rewrite - qb in he. have fm i j: i <c j -> j <c n -> glt r (Vg f i) (Vg f j). move => lij jd; move: (NS_lt_nat jd nN) => jN; move: j jN lij jd. apply: Nat_induction; first by move/clt0. move => j jN Hrec lij ljd; move: (proj1 (he 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). have ww: range f =c E. by rewrite - (consec_pow_pr2 or qa) - qb /n double_cardinal. move:(strict_sub_smaller_contra fse hc ww) => rf. split => // u v ; rewrite - /E - rf; move => uu; move: uu (uu). move => /(range_gP ha) [i idf ->] uu /(range_gP ha) [j jdf ->]. move: idf jdf; rewrite - qb; move/(NltP nN) => lin; move/(NltP nN) => ljn. case: (cleT_ell (proj31_1 lin)(proj31_1 ljn)) => cp. - by rewrite - cp; left; order_tac; apply: hc. - left; exact: (proj1 (fm i j cp ljn)). - right; exact: (proj1 (fm j i cp lin)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)