proposition: Lemma Exercise1_19a: without_gaps (order_sum r g) <-> [/\ (exists i j, glt r i j) \/ (exists i x y, inc i (substrate r) /\ glt (Vg g i) x y), (forall i x y, inc i (substrate r) -> glt (Vg g i) x y -> without_gaps (Vg g i)) & (forall i j, glt r i j -> [\/ (exists2 k, glt r i k & glt r k j), (forall u, ~ (maximal (Vg g i) u)) | (forall u, ~ (minimal (Vg g j) u))])].
proof: Proof. move: (ax) => [q1 q2 q4];split. move=>[or [x1 [y1 x1y1]] wg]; split. + move: x1y1 => [] /orsum_gleP [p1 p2 p3] di. case: p3; first by move=> h; left; exists (Q x1), (Q y1). move=> [sq1 cp]; right; exists (Q x1); exists (P x1), (P y1). move: (du_index_pr1 p1) (du_index_pr1 p2) => [a1 a2 a3][a4 a5 a6]. by rewrite q2; split => //; split => // ; dneg sq; apply: pair_exten. + move => i x y isr lt1; split => //; first by apply: q4; ue. by exists x, y. move=> u v [leuv neuv]. rewrite q2 in isr. have lt2: (glt (order_sum r g) (J u i) (J v i)). split; last by dneg sj; apply: (pr1_def sj). apply /orsum_gleP; split => //; last (by right; aw); apply: disjoint_union_pi1=>//; order_tac. move: (wg _ _ lt2) => [z [zl1 zne1] [zl2 zne2]]. move: (orsum_gle_id ax zl1)(orsum_gle_id ax zl2); aw => lea leb. move: (order_antisymmetry q1 lea leb) => lec. move: zl1 zl2 => /orsum_gleP [_ zs zl1] /orsum_gleP [_ _ zl2]. move: (du_index_pr1 zs)=> [a1 a2 a3]. exists (P z); rewrite /glt;split => //. - by case: zl1;case; aw; rewrite - lec. - move=> upz; case: zne1; apply: pair_exten; aww. - by case: zl2;case; rewrite - lec; aw. - move=> upz; case: zne2; apply: pair_exten; aww. + move=> i j ij. case: (p_or_not_p (exists u, maximal (Vg g i) u)); last first. by move => bad; constructor 2 => u mu; case: bad; exists u. case: (p_or_not_p (exists v, minimal (Vg g j) v)); last first. by move => bad _; constructor 3 => v mu; case: bad; exists v. move => [v [vs vm]] [u [us um]]. have idf: (inc i (domain g)) by rewrite -q2; order_tac. have jdf: (inc j (domain g)) by rewrite -q2; order_tac. have J1: (inc (J u i) (sum_of_substrates g)) by apply: disjoint_union_pi1. have J2: (inc (J v j) (sum_of_substrates g)) by apply: disjoint_union_pi1. have l1: (glt (order_sum r g) (J u i) (J v j)). split; first by apply/orsum_gleP; split => //; left; aw. move=> sj; move: ij => [_]; case; apply: (pr2_def sj). move: (wg _ _ l1) => [z [z1 z2] [z3 z4]]. move: z1 z3 =>/orsum_gleP [_ zs z5] /orsum_gleP [_ _ z6]. move: (du_index_pr1 zs)=> [a1 a2 a3]. case: z5; rewrite pr2_pair => a4. case: z6; rewrite pr2_pair => a5; first by constructor 1; exists (Q z). move: a5 => [Qa]; rewrite pr1_pair Qa => Pa. move: (vm _ Pa) => pz; case: z4; apply: pair_exten; aww. move: a4 => [Qa]; rewrite pr1_pair => Pa. move: (um _ Pa) => pz; case: z2; apply: pair_exten; aww. move=> [CI CII CIII]. have os: order (order_sum r g) by fprops. split => //. case: CI. move=> [i [j ij]]. have idf: (inc i (domain g)) by rewrite -q2; order_tac. have jdf: (inc j (domain g)) by rewrite -q2; order_tac. move: (ax2 idf)(ax2 jdf) => [u us] [v vs]. have J1: (inc (J u i) (sum_of_substrates g)) by apply: disjoint_union_pi1. have J2: (inc (J v j) (sum_of_substrates g)) by apply: disjoint_union_pi1. have l1: (glt (order_sum r g) (J u i) (J v j)). split; first by apply /orsum_gleP; split => //; left; aw. move=> sj; case: (proj2 ij); apply: (pr2_def sj). by exists (J u i); exists (J v j). move=> [i [u [v [isr [leij neij]]]]]. rewrite q2 in isr; move: (q4 _ isr) => oi. exists (J u i); exists (J v i);split; last by dneg sj; apply: (pr1_def sj). apply /orsum_gleP; split => //; last (by right; aw); apply: disjoint_union_pi1 => //; order_tac. move=> x y [lexy nexy]; move: lexy => /orsum_gleP //. move=> [xsr ysr lexy]. move: (du_index_pr1 xsr) (du_index_pr1 ysr)=> [a1 a2 a3][a4 a5 a6]. case: lexy => lea. case: (CIII _ _ lea). + move=> [k k1 k2]. have ksr: (inc k (domain g)) by rewrite -q2; order_tac. move: (ax2 ksr) => [z zs]. have J1: (inc (J z k) (sum_of_substrates g)) by apply: disjoint_union_pi1. have xn: x <> J z k by move: k1 =>[_ Qx]; dneg xj;rewrite xj; aw. have yn: J z k <> y by move: k2 =>[_ Qx]; dneg xj;rewrite - xj; aw. by exists (J z k); split => //; apply /orsum_gleP; split => //; left; aw. + move => nmm; move: (nmm (P x)); rewrite /maximal => nm. have [z zs pz]: (exists2 z, inc z (substrate (Vg g (Q x))) & glt (Vg g (Q x)) (P x) z). ex_middle ww; case: nm; split => // z z1. case:(equal_or_not (P x) z) => // pzx; case: ww; exists z => //;order_tac. have J1:inc (J z (Q x)) (sum_of_substrates g) by apply: disjoint_union_pi1. have xn: x <> J z (Q x) by move: pz =>[_ Qx]; dneg xj;rewrite xj; aw. have yn: J z (Q x) <> y by move: lea =>[_ Qx]; dneg xj;rewrite - xj; aw. exists (J z (Q x)); split => //; apply /orsum_gleP;split => //. by right; aw; move: pz => [pz _]. by left; aw. + move => nmm;move: (nmm (P y)); rewrite /minimal => nm. have [z zs pz]: (exists2 z, inc z (substrate (Vg g (Q y))) & glt (Vg g (Q y)) z (P y)). ex_middle ww; case: nm;split => // z zl. case: (equal_or_not z (P y)) => // pzx; case: ww;exists z => //;order_tac. have J1: inc (J z (Q y)) (sum_of_substrates g) by apply: disjoint_union_pi1. have xn: x <> J z (Q y) by move: lea =>[_ Qx]; dneg xj;rewrite xj; aw. have yn: J z (Q y) <> y by move: pz =>[_ Qx]; dneg xj;rewrite - xj; aw. exists (J z (Q y)); split => //; apply /orsum_gleP; split => //. by left; aw. by right; aw; move: pz => [pz _]. move: lea => [qxy sv]. have lv1: (glt (Vg g (Q x)) (P x) (P y)). by split=>//; dneg h; apply: pair_exten. have qsr: (inc (Q x) (substrate r)) by ue. move: (CII _ _ _ qsr lv1) => [w1 w2 w3]. move: (w3 _ _ lv1) => [z [z1 z2] [z3 z4]]. have zs: inc z (substrate (Vg g (Q x))) by order_tac. have J1: inc (J z (Q x)) (sum_of_substrates g) by apply: disjoint_union_pi1. have xn: x <> J z (Q x) by move=> xe; case: z2;rewrite xe; aw. have yn: J z (Q x) <> y by move=> xe; case: z4;rewrite - xe; aw. by exists (J z (Q x)); split => //;apply /orsum_gleP; split => //;right; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)