proposition: Lemma IFE_consecP x y : inc x IFSE -> inc y IFSE -> ((consecutive IFS_order x y) <-> [/\ P (P x) = P (P y), Q x = Q y & csucc (Q (P x)) = Q (P y)]).
proof: Proof. move =>xE yE. move/Zo_P: (xE) => [/setX_P [ra /setX_P [rb rc rd] re] rf]. move/Zo_P: (yE) => [/setX_P [ra' /setX_P [rb' rc' rd'] re'] rf']. split. set a := (P (P x)); set b := (Q (P x)); set c := Q x. move => [/IFE_gltP qa qb]. case: (proj33 qa). + move => lt0. move: (qlt_succ re) => la. move: (proj32_1 la) => ccq. set z := J (J a b) (c +q \1q). have zE: inc z IFSE. apply/Zo_P; split; first by apply: setXp_i => //; apply: setXp_i. by rewrite /z; aw; rewrite rb. have zs: inc z (substrate IFS_order) by rewrite (proj2 (IFE_osr)). have lt3: glt IFS_order x z. by apply/IFE_gltP; split => //; constructor 2; rewrite /z;split; aw. have lt4: glt IFS_order z y. by apply/IFE_gltP; split => //; constructor 1; rewrite /z; aw. by case: (qb z zs). + move => [eq1 lt1]. move: (BQmiddle_comp lt1) => [lt2 lt3]. move: (proj31_1 lt3) => cc. set z := J (J a b) (BQmiddle (Q x) (Q y)). have zE: inc z IFSE. apply/Zo_P; split; first by apply: setXp_i => //; apply: setXp_i. by rewrite /z; aw; rewrite rb. have zs: inc z (substrate IFS_order) by rewrite (proj2 (IFE_osr)). have lt4: glt IFS_order x z. apply/IFE_gltP; split => //; constructor 2; rewrite /z;saw. have lt5: glt IFS_order z y. apply/IFE_gltP; split => //; constructor 2; rewrite /z;saw. by case: (qb z zs). + move => [eq1 eq2 lt1]; split => //. move /(cleSltP rd): (lt1). case/cle_eqVlt => // lt2. set z := J (J a (csucc b)) c. move:(NS_succ rd) => cc. have zE: inc z IFSE. apply/Zo_P; split; first by apply: setXp_i => //; apply: setXp_i. rewrite /IFS_good_pair; rewrite /z; aw. by move: (proj1 (clt_leT lt2 rf')); rewrite - eq1. have zs: inc z (substrate IFS_order) by rewrite (proj2 (IFE_osr)). have lt4: glt IFS_order x z. apply/IFE_gltP; split => //; constructor 3; rewrite /z;saw. by apply: cltS. have lt5: glt IFS_order z y. apply/IFE_gltP; split => //; constructor 3; rewrite /z;saw. by case: (qb z zs). move => [ha hb hc]; split. apply /IFE_gltP; split => //; constructor 3; split => //. by rewrite - hc; apply: cltS. move => z; rewrite (proj2 (IFE_osr)) => zE [za zb]. move/IFE_gltP: za => /proj33 zc; move/IFE_gltP: zb => /proj33 zd. case: zc; case: zd. - by rewrite - ha => /proj1 aa/cltNge; case. - by move => [-> _]; rewrite ha; case. - by move => [-> _] _; rewrite ha; case. - by rewrite ha; move => [_ qa][qb _]; case: qa. - by rewrite hb; move => [_ qa][_] /proj1/ qleNgt; case. - by rewrite hb; move => [_ -> _] [_ /proj2]; case. - by rewrite ha; move => /proj2 bb /proj31 eq; case:bb. - by rewrite hb; move => [_ /proj2 bb] /proj32 eq; case: bb. - by rewrite - hc; move => /proj33 /(cltSleP rd) la /proj33 /cltNge; case. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)