proposition: Lemma Exercise4_10a r n: order r -> inc n Nat -> n <> \0c -> Ex4_10_hyp r n -> Ex4_10_conc r n.
proof: Proof. move => or nN nnz [g [A [f [ofg alt cdg saf isf]]]]. have [h [bh sh th]]: exists h, bijection_prop h (Nint n) (domain g). by apply /card_eqP; rewrite (card_Nint nN) cdg. move: (Nintco_wor n) => []. set rI := Nint_co n; move => worI srI. pose hk k := (h \co shift_mod_n n k). have bcs: forall k, k<c n -> substrate rI = source (hk k). by move => k kn; rewrite /hk /shift_mod_n; aw. have bcp: forall k, k<c n -> (h \coP shift_mod_n n k /\ bijection (hk k)). move => k kn. move: (shift_mod_n_fb nN nnz kn) => bs. have pa: h \coP shift_mod_n n k. by split => //; try fct_tac; rewrite /shift_mod_n; aw. by split => //; apply: compose_fb. pose ork k := Vfs (ext_to_prod (hk k) (hk k)) rI. have orkp: forall k, k<c n -> [/\ substrate (ork k) = domain g, order_isomorphism (hk k) rI (ork k) & worder (ork k)]. move => k kn. have aux := (conj (proj1 worI) (bcs _ kn)). move: (order_transportation (proj2 (bcp _ kn)) aux). rewrite -/(ork k) => is1; split => //. by move: (is1) => [_ _[_ _ <-] _]; rewrite {1} /hk; aw. by apply: (worder_invariance _ worI); exists (hk k). pose opk k := order_prod (ork k) g. have opk_ax: forall k, k <c n -> orprod_ax (ork k) g. by move => k kn; move: (orkp _ kn) => [sr _ wo]. have opk_total: forall k, k <c n -> total_order (opk k). move => k kn;move: (opk_ax _ kn) => ax; apply: orprod_total=> //. set F := substrate (order_product g). move: (order_product_osr ofg) => [pa pb]. have opksr: forall k, k<c n -> substrate (opk k) = F. move => k kn; move: (opk_ax _ kn) => ax. rewrite /opk /F orprod_sr // pb //. have oplc1: forall k, k <c n -> sub (order_product g) (opk k). move => k kn t t1. move:pa => [kg _ _ _]. move: (kg _ t1) => pt; move: t1; rewrite - pt. set x := P t; set y:= Q t. move /order_product_gleP=> [xp yp lexy];apply /(orprod_gle1P (opk_ax _ kn)). move: (orkp _ kn) => [srd _ [ok _]]. have sa: sub (Zo (domain g) (fun i => Vg x i <> Vg y i)) (substrate (ork k)). rewrite srd; apply: Zo_S. split => //; move => j []; rewrite (iorder_sr ok sa). move /Zo_P =>[s1 s2]; split => //; by apply: lexy. have lt0n: \0c <c n by apply /strict_pos_P1. have zi: inc \0c (Nint n) by apply /NintP. have ne1: nonempty (Lg (Nint n) opk). by exists (J \0c (opk \0c)); apply /funI_P; exists \0c. have conc1: (order_product g) = intersectionb (Lg (Nint n) opk). set_extens t. move => tg; apply /(setIb_P ne1); aw => i ib; rewrite LgV//. by move/(NintP nN): ib => lin; apply (oplc1 _ lin). move /(setIb_P ne1); aw => h1; move: (h1 _ zi); rewrite LgV// => tz. move: (opk_total _ lt0n) => [[gr0 _] _]. move: (gr0 _ tz); rewrite /pairp; set x := P t; set y:= Q t => eq1. have pa': forall i, i <c n -> gle (opk i) x y. move => i lin. have lic: inc i (Nint n) by apply /(NintP nN). move: (h1 _ lic); rewrite - eq1;rewrite LgV//. move: (pa' _ lt0n) => /(orprod_gleP (opk_ax _ lt0n)) [xsr ysr _ _ _]. rewrite - eq1; apply /order_product_gleP;split => //; move => i idg. have pc: gle (Vg g i) (Vg x i) (Vg x i). move: xsr => /prod_of_substratesP [fgx dx hx]. move: (hx _ idg) (ofg _ idg) => xsr1 odg. by order_tac. move: (idg); rewrite -th => idh. move: (bij_surj bh idh) => [k]; rewrite sh => /(NintP nN) kn Wk. move: (pa' _ kn) => /(orprod_gleP (opk_ax _ kn)) [_ _ ww]. case: ww; first by move => <-. move => [j [jsk lta lea]]. case: (equal_or_not i j); first by move => ->; exact (proj1 lta). move => ij. move: (orkp _ kn) => [sa [_ _ [bk sk tk] mk] sc]. rewrite - tk in jsk. move: (bij_surj bk jsk) => [ja jas jav]. have zl1: gle rI \0c ja. apply /(Nintco_gleP nN). move: jas; rewrite sk srI; move /(NintP nN)=> jn;split => //. apply: (cle0x (proj31_1 jn)). hnf in mk;rewrite sk srI in mk jas. move: (proj1 (bcp _ kn)) => cop. have zs1:inc \0c (source (shift_mod_n n k)) by rewrite /shift_mod_n; aw. move: (mk _ _ zi jas); rewrite - jav /hk; rewrite compfV//. move: (shift_mod_n_ax nN nnz (NS_le_nat (proj1 kn) nN)) => ta. rewrite /shift_mod_n (LfV ta zi) (shift_mod_n_vl nN nnz kn lt0n). have ck := proj31_1 kn. rewrite csum0l//; Ytac0; move => eqv; move: (proj1 eqv zl1). by rewrite -Wk => aux; rewrite - (lea _ (conj aux ij)). pose opkA k := induced_order (opk k) A. have altA: forall k, k <c n -> (total_order (opkA k)). move => k kn; move: (opk_total _ kn) => to1. by apply: total_order_sub => //; rewrite (opksr _ kn). have opkAi: (induced_order (order_product g) A) = intersectionb (Lg (Nint n) opkA). rewrite /opkA /induced_order conc1. have ne2:nonempty (Lg (Nint n) (fun k => opk k \cap coarse A)). by exists (J \0c((opk \0c) \cap coarse A)); apply /funI_P; exists \0c. move :(setIb_P ne2) (setIb_P ne1); aw => ia ib. set_extens t. move => /setI2_P [ta tb]; apply /ia => i id; rewrite LgV//. by apply /setI2_P;split => //; move /ib: ta; aw => k; move: (k _ id); rewrite LgV//. move => pa'; apply /setI2_P; move /ia: pa' => k; split. by apply/ib => i id;rewrite LgV//; move: (k _ id); rewrite LgV// => /setI2_P []. by move: (k _ zi); rewrite LgV// => /setI2_P []. move: (isf) => [_ _ [bf _ _]_]. move: (inverse_bij_fb bf) => bif. set ibf := (inverse_fun f). pose orkE k := Vfs (ext_to_prod ibf ibf) (opkA k). have qa: order (order_product g) by apply (proj1 (order_product_osr ofg)). move: (iorder_osr qa saf) => [qb qb']. have qc: A = target f. by move: isf => [_ _ [_ _ tf] _ ]; rewrite tf qb'. have qd: substrate (induced_order (order_product g) A) = source ibf. by rewrite iorder_sr //; rewrite /ibf; aw. set orkEi := Vfs (ext_to_prod ibf ibf) (induced_order (order_product g) A). have orkEip: order_isomorphism ibf (induced_order (order_product g) A) orkEi. by apply: order_transportation. have eq0: orkEi = r. move: orkEip => [o1 o2 [bk sk tk] mk]. move: isf => [_ _ [_ sf tf] mf]. have tibf: target ibf = source f by rewrite /ibf; aw. have sibf: source ibf = target f by rewrite /ibf; aw. hnf in mk; rewrite sibf in mk. have ffi: forall z, inc z (source f) -> (inc (Vf f z) (target f) /\ Vf ibf (Vf f z) = z). move => e zf;split; [ Wtac; fct_tac | by rewrite inverse_V2]. apply: order_exten => // => x y; split => cp1. have xs: inc x (substrate orkEi) by order_tac. have ys: inc y (substrate orkEi) by order_tac. rewrite - tk tibf in xs ys. move: (ffi _ xs) (ffi _ ys) => [pa' pb'] [pc pd]. by rewrite (mf _ _ xs ys) (mk _ _ pa' pc) pb' pd. have xs: inc x (substrate r) by order_tac. have ys: inc y (substrate r) by order_tac. rewrite - sf in xs ys. move: (ffi _ xs) (ffi _ ys) => [pa' pb'] [pc pd]. by move: cp1; rewrite (mf _ _ xs ys) (mk _ _ pa' pc) pb' pd. have orkEp: forall k, k<c n -> [/\ substrate (orkE k) = substrate r, order_isomorphism ibf (opkA k) (orkE k) & total_order (orkE k)]. move => k kn. move: (altA _ kn) => tor; move: (tor) => [ok _]. move: (opk_total _ kn) (opksr _ kn) => [orkn _] srkn. have srk: substrate (opkA k) = source ibf. by rewrite /ibf; aw;rewrite -qc /opkA iorder_sr // srkn. move: (order_transportation bif (conj ok srk)). rewrite -/ibf -/(orkE k) => ois. move: (ois) => [_ o2 [bk sk tk] mk]. have sr1: substrate (orkE k) = substrate r. by rewrite - tk /ibf; aw; move: isf => [_ _ [_ <- _]_]. split => //; split; [ exact | move => x y xsr ysr]. rewrite - tk in xsr ysr. move: (bij_surj bk xsr) => [x' x's ->]. move: (bij_surj bk ysr) => [y' y's ->]. move: tor => [_]; rewrite - sk => tor. by case: (tor _ _ x's y's); rewrite mk // => cp1; [left | right]. set G := Lg (Nint n) orkE. have c0: forall i, inc i (domain G) -> [/\ order (Vg G i), total_order (Vg G i) &substrate (Vg G i) = substrate r]. rewrite /G; aw => i idg; rewrite LgV//; move: idg => /(NintP nN) idg. by move: (orkEp _ idg) => [ta [_ tb]];split => //; move: tb => []. have c1: order_fam G by move => i idg; move: (c0 _ idg) => [ok _]. have c2: (allf G total_order) by move => i idg; move: (c0 _ idg) => [_ ok _ ]. have c3: cardinal (domain G) = n by rewrite /G; aw; rewrite card_Nint. have c4: forall i, inc i (domain G) -> substrate (Vg G i) = substrate r. by move => i idg; move: (c0 _ idg) => [_ _ ok ]. exists G;split => //. rewrite -eq0 /orkEi opkAi /G /orkE. have fif: injection ibf by move: bif => []. move: (ext_to_prod_fi fif fif); set hf := (ext_to_prod ibf ibf) => fh. rewrite /intersectionb (inj_image_setIf _ _ fh). have ne2: nonempty (Nint n) by exists \0c; aw. aw; set_extens t; move => /(setIt_P _ ne2) hp; apply /(setIt_P _ ne2) => j; move: (R_inc j) => ri; move: (hp j); rewrite !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)