proposition: Lemma Exercise1_6s: nonempty E -> nonempty F -> (total_order (increasing_mappings_order r r') <-> [\/ singletonp F, (singletonp E /\ total_order r') | [/\ total_order r', total_order r & exists u v, F = doubleton u v]]).
proof: Proof. move=> ne1 ne2. split;last first. case; first by apply: Exercise1_6p. by move=> [h1 h2];apply: Exercise1_6q. by move=> [h1 [h2 h3]]; apply: Exercise1_6r. move => tor; move: (Exercise1_6o ne1 tor) => tor'. move: (tor') => [_ tor'']. move: (ne2) => [y yF]. case: (equal_or_not F (singleton y))=> Fp; first by constructor 1; exists y. move: (ne1) => [z zE]. case: (equal_or_not E (singleton z))=> Ep. by constructor 2; split => //;exists z. constructor 3. have [y' yF' yy']: (exists2 y1, inc y1 F & y1 <> y). ex_middle h; case: Fp; set_extens t. case: (equal_or_not t y); first by move => ->; fprops. move => ty ts; case: h;ex_tac. by move /set1_P => ->. have [a [b [aF bF ltab]]]: exists a b, [/\ inc a F, inc b F & glt r' a b]. case: (tor'' _ _ yF yF'). by move => aux; exists y, y'; split => //; split => //; apply:nesym. rewrite /glt;move => aux; exists y', y;split => //. clear yF yF' Fp yy' y y'. set sf:= fun x a b u => Yo (gle r u x) a b. have sfa: forall x a b, inc a F -> inc b F -> (lf_axiom (sf x a b) E F). by rewrite /sf=> x v w vF wF u uE; case: (p_or_not_p (gle r u x)) => h; Ytac0. have sfb: forall x a b, inc a F -> inc b F -> glt r' a b -> (inc (Lf (sf x a b) E F) (increasing_mappings r r')). move => x a' b' aF' bF' latab'; move: (sfa x _ _ aF' bF') => ta. move: (lf_function ta) => fb. apply /soimP => //;saw; saw; first saw. move=> u v uv. have us: (inc u E) by rewrite /E;order_tac. have vs: (inc v E) by rewrite /E;order_tac. rewrite LfV // LfV // /sf. case: (p_or_not_p (gle r u x)) => ux; Ytac0; case: (p_or_not_p (gle r v x)) => vx; Ytac0; try order_tac => //. case: ux; order_tac. have to: (total_order r). split=> //; rewrite -/E => x y xsr ysr. move: (sfb x _ _ aF bF ltab) (sfb y _ _ aF bF ltab) => fx fy. move: tor => [_]; rewrite (proj2 (imo_osr r or')) => aux; red. case: (p_or_not_p (gle r x y)); first by left. case: (p_or_not_p (gle r y x)); first by right. move=> be1 be2. have sfxx: sf x a b x = a by rewrite /sf Y_true //; order_tac. have sfyy: sf y a b y = a by rewrite /sf Y_true //; order_tac. have sfxy: sf x a b y = b by rewrite /sf Y_false//; order_tac. have sfyx: sf y a b x = b by rewrite /sf Y_false//; order_tac. move: (sfa x _ _ aF bF)(sfa y _ _ aF bF) => h1 h2. case: (aux _ _ fx fy) => h; move : (imo_incr or' h xsr) (imo_incr or' h ysr); rewrite !LfV// sfxx sfyx sfyy sfxy; move=> h3 h4; order_tac. split => //. case: (equal_or_not F (doubleton a b)); first by move=> h; exists a,b. move=> at2. have at3: exists c, [/\ inc c F, c <> a & c <> b]. ex_middle at3; case: at2; set_extens t. case: (equal_or_not t a); first by move => ->; fprops. case: (equal_or_not t b); first by move => ->; fprops. by move => tb ta ts; case: at3; exists t. by case/set2_P => ->. have [u [v [w [uF vF wF uv vw]]]]: (exists u v w, [/\ inc u F, inc v F, inc w F, glt r' u v & glt r' v w]). move: at3 => [c [cF ca cb]]; case: (tor'' _ _ cF aF)=> lca. by exists c, a, b. case: (tor'' _ _ bF cF) => lbc. by exists a, b, c; split => //; split => //;apply:nesym. by exists a, c, b; split => //; split => //; apply:nesym. set (f:= constant_function (substrate r) F v). have fs:(inc f (increasing_mappings r r')) by apply: constant_increasing. have [z' zE' zz']: (exists2 y1, inc y1 E & y1 <> z). ex_middle h; case: Ep; set_extens t. case: (equal_or_not t z); first by move => ->; fprops. move => ty ts; case: h; ex_tac. by move /set1_P => ->. have [i [s [iF sF ltis]]]: exists i s, [/\ inc i E, inc s E & glt r i s]. move: to => [_ to];case: (to _ _ zE zE'). by move => aux; exists z, z';split => //; split => //; apply:nesym. rewrite /glt; move => aux; exists z', z;split => //. have ltuv: glt r' u w by order_tac. move: (sfa i u w uF wF) (sfb i u w uF wF ltuv). set g:= Lf _ _ _; move=> ta fg. move: tor => [_]; rewrite (proj2 (imo_osr r or')) => aux. have p1: Vf f i = v by rewrite /f constant_V. have p2: Vf f s = v by rewrite /f constant_V. have p3: Vf g i = u by rewrite /g /sf LfV// Y_true//; order_tac. have p4: Vf g s = w by rewrite /g /sf LfV // Y_false// => h; order_tac. case: (aux _ _ fs fg) => h; move: (imo_incr or' h iF) (imo_incr or' h sF); rewrite p1 p2 p3 p4 => p5 p6; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)