proposition: Lemma Exercise1_22d x u1 u2: open_o r x -> open_r r u1 -> open_r r u2 -> cofinal (induced_order r u1) x -> cofinal (induced_order r u2) x -> u1 = u2.
proof: Proof. move=> ox [ou1 pu1] [ou2 pu2] co1 co2. move: (Exercise1_22a ou1 ou2). move: (@subsetU2l u1 u2) (@subsetU2r u1 u2). set (u3:= u1 \cup u2) => su1 su2 ou3. have su3: (sub u3 (substrate r)) by move: ou3 => [ok _]. have su1r: (sub u1 (substrate r)) by move: ou1 => [ok _]. have su2r: (sub u2 (substrate r)) by move: ou2 => [ok _]. move: co1 co2 => /(cofinal_inducedP su1r) [xu1 co1] /(cofinal_inducedP su2r) [xu2 co2]. have co31:(cofinal (induced_order r u3) u1). apply/cofinal_inducedP => //; split => // t /setU2_P; case. by move => tu1; ex_tac; order_tac; apply: su1r. move/co2 => [y /xu1 ya yb]; ex_tac. rewrite(pu1 _ ou3 co31). have co32:(cofinal (induced_order r u3) u2). apply/cofinal_inducedP => //; split => // t /setU2_P; case. move/co1 => [y /xu2 ya yb]; ex_tac. by move => tu1; ex_tac; order_tac; apply: su2r. by rewrite (pu2 _ ou3 co32). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)