proposition: Lemma OT_of_E: order_type_of IFS_order = sier_inf_sum sigma.
proof: Proof. rewrite sier_inf_sum_prop. apply: order_type_unique. move: IFE_osr => [or1 sr1]. move: Nat_order_wor => [[or2 _] sr2]. have or5 := BQor_or. set g1 := Lg Nat (sier_inf_sum_aux sigma). have aux: order_fam (Lg Nat (sier_inf_sum_aux sigma)). hnf; aw => t tN; rewrite LgV//; apply: (orprod2_or _ BQor_or). apply: ordinal_o_or. have ax: orsum_ax Nat_order g1. rewrite /g1; saw; hnf;aw => y yN; rewrite LgB//. move:(orsum_osr ax) =>[or3 sr3]. set F := sum_of_substrates g1. pose h x := J (variantLc (Q x) (Q (P x)) ) (P (P x)). have axs n: natp n -> natp (Vf sigma n). move /permutationsP: sp => [[[ff _] _] sf tf] sn. rewrite /natp; Wtac; ue. have vs x: inc x IFSE -> inc (variantLc (Q x) (Q (P x))) (substrate (sier_inf_sum_aux sigma (P (P x)))). move/Zo_P => [/setX_P [ra /setX_P [rb rc rd] re] rf]. have Ha: order (ordinal_o (csucc (Vf sigma (P (P x))))). by apply: ordinal_o_or. rewrite /sier_inf_sum_aux. rewrite (orprod2_sr Ha BQor_or) BQor_sr ordinal_o_sr. apply/setX2_P; aw; split => //; fprops. by apply/(NleP (axs _ rc)). have ax2 x: inc x IFSE -> inc (h x) F. move => xx; move: (vs _ xx) => ra. move/Zo_P: xx => [/setX_P [_ /setX_P [_ rc rd] re] _]. by apply: disjoint_union_pi1; rewrite /g1; aw; bw. have hbp:bijection_prop (Lf h IFSE F) IFSE (sum_of_substrates g1). saw; apply : lf_bijective. - done. - move => x y. move/Zo_P => [/setX_P [ra /setX_P [rb rc rd] re] rf]. move/Zo_P => [/setX_P [sa /setX_P [sb sc sd] se] sf]. move/pr12_def => [eq1 eq2]. move: (f_equal (Vg ^~ C0) eq1) (f_equal (Vg ^~ C1) eq1); aw => eq3 eq4. by apply: pair_exten => //; apply: pair_exten. - move => y /du_index_pr1 [ea eb ec]. have oo : order (ordinal_o (csucc (Vf sigma (Q y)))) by apply: ordinal_o_or. move: ea; rewrite /g1; aw => ea. move: eb; rewrite /g1/sier_inf_sum_aux; rewrite LgV// orprod2_sr //. rewrite BQor_sr ordinal_o_sr; move/setX2_P =>[qa qb qc qd]. move: (axs _ ea) => sn. move/(NleP sn): qd => le1. move: (NS_le_nat le1 sn) => rn. exists (J (J (Q y) (Vg (P y) C1)) (Vg (P y) C0)). apply: Zo_i. by apply: setXp_i => //; apply: setXp_i. by rewrite /IFS_good_pair; aw. rewrite /h; aw; rewrite -{1} ec; congr J. apply: fgraph_exten; aww. by rewrite qb => t; case /set2_P => ->; aw. exists (Lf h IFSE F); split => //. by rewrite sr1 sr3. hnf; aw => x y xE yE; rewrite ! LfV//. apply: (iff_trans (IFE_gleP x y)). apply: iff_trans (iff_sym (orsum_gleP Nat_order g1 (h x) (h y))). have ha: inc (h x) (sum_of_substrates g1) by apply: ax2. have hb: inc (h y) (sum_of_substrates g1) by apply: ax2. move/Zo_P:(xE) => [/setX_P [ra /setX_P [rb rc rd] re] rf]. move/Zo_P:(yE) => [/setX_P [sa /setX_P [sb sc sd] se] sf]. have or4: order (ordinal_o (csucc (Vf sigma (P (P x))))). by apply: ordinal_o_or. have or6: order (ordinal_o (csucc (Vf sigma (P (P y))))). by apply: ordinal_o_or. move: (vs _ xE) (vs _ yE); rewrite /sier_inf_sum_aux. rewrite (orprod2_sr or4 or5) (orprod2_sr or6 or5) => Vx Vy. split; move => [_ _ hc]; split => //. hnf; rewrite /h; aw; case: hc. - move =>[la lb]; left; split => //; apply /Nat_order_leP. split => //. - move =>[la lb]; right; split => //. rewrite /g1/sier_inf_sum_aux LgV//. apply /(orprod2_gleP or4 or5); aw. split; [ done | by rewrite la | by right; apply /BQlt_P]. - move =>[la lb lc]; right; split => //. rewrite /g1/sier_inf_sum_aux LgV//. apply /(orprod2_gleP or4 or5); aw. split => //; first by rewrite la. left; split => //; apply/ordo_leP. move: (axs _ sc) => xx. move/(NleP xx) : (cleT lc sf) => rr2. move/(NleP xx) : sf => rr1. rewrite la; split => //; exact: (proj33 lc). case: hc. move => [/Nat_order_leP [_ _ ]]; rewrite /h; aw => ma mb. by constructor 1. rewrite /h; aw. move => [a]; rewrite /g1/sier_inf_sum_aux LgV//. move /(orprod2_gleP or4 or5); move =>[ _ _]; aw; case. move =>[lb /ordo_leP [lc ld le]]. constructor 3; split => //. move: (axs _ rc) => sn. move/(NleP sn):lc => /proj31 ca. move/(NleP sn):ld => /proj31 cb. by split. by move/BQlt_P => lc; constructor 2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)