proposition: Lemma Exercise1_6r: total_order r -> total_order r' -> (exists a b, F = doubleton a b) -> total_order (increasing_mappings_order r r').
proof: Proof. move=> [_ tor] [_ tor'] [u [v sr']]. case: (equal_or_not u v) => uv. by apply: Exercise1_6p => //; rewrite sr' -uv; exists u. have [a [b [ab aF bF ltab]]]: exists a b, [/\ F = doubleton a b, inc a F, inc b F & glt r' a b]. have ap: (inc u F) by rewrite sr'; fprops. have bp: (inc v F) by rewrite sr'; fprops. case: (tor' _ _ ap bp) => le1. exists u, v; split => //; split =>//. by exists v, u; rewrite set2_C; split => //; split =>//; apply:nesym. clear sr' uv u v. move: (imo_osr r or') => [pa1 pb1]. split => //. rewrite pb1; move=> x y xs ys; rewrite /ocomparable. move: (xs)(ys) => /soimP [[fx sx tx] ix] /soimP [[fy sy ty] iy]. have Ha: forall c, inc c E -> (inc (Vf x c) F) /\ (inc (Vf y c) F). move => c cE; rewrite /F -{1} tx - ty;split; apply: Vf_target =>//; ue. have aux: (forall t, inc t E -> glt r' (Vf x t) (Vf y t) -> (Vf x t = a /\ Vf y t = b)). move=> t tsr wt; move: (Ha _ tsr) (wt) => []. rewrite -/F ab; case /set2_P => -> ; case /set2_P => -> //; [by case | by move => [ha _]; order_tac | by case]. case: (p_or_not_p (exists2 u, inc u E & glt r' (Vf x u) (Vf y u))). move=> [u usr uwy]; left. apply /imo_gleP => //; split => //; split => // i isr. move: (Ha _ isr) => [];rewrite ab; case /set2_P => h1; case /set2_P => h2; rewrite h1 h2;try order_tac => //. move: (aux _ usr uwy) => [h3 h4]. move: ix iy => [_ _ _ ix] [_ _ _ iy]. by case: (tor _ _ usr isr) => h5; move: (ix _ _ h5) (iy _ _ h5); rewrite h2 h3 h4 h1. move=> neu; right; apply /imo_gleP => //; split => //;split => //. move=> i isr;move: (Ha _ isr) => [xw yw]. case: (tor' _ _ xw yw) => //. case: (equal_or_not (Vf x i) (Vf y i)) =>sw; first by rewrite sw. by move=> nle; case: neu; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)