proposition: Lemma Exercise2_1c r: order r -> r = intersection (Zo (orders (substrate r)) (fun r' => total_order r' /\ sub r r')).
proof: Proof. move=> or; set bs:= Zo _ _. move: (order_total_extension or) => [r' [tor' sr' sr]]. have rb': (inc r' bs). by apply: Zo_i => //; apply /ordersP; split => //; move: tor'=> [or'_ ]. set_extens t. move => tr;apply: setI_i;first by ex_tac. by move=> y => /Zo_hi [_ ]; apply. move=> tb; move: (setI_hi tb rb') => tr'. move: tor'=> [or' tor']. have pt: (pairp t) by apply: (order_sgraph or'). have tp: (t = J (P t) (Q t)) by aw. rewrite tp in tr'. have p1: (inc (P t) (substrate r)) by rewrite - sr'; substr_tac. have p2: (inc (Q t) (substrate r)) by rewrite - sr'; substr_tac. case: (p_or_not_p (gle r (P t) (Q t))); first by rewrite /gle/related -tp. move=> grqp. move:(Exercise2_1a or p2 p1 grqp)=> /=. set r'':= union2 _ _. move => [] /fo_gleP [_ or'' _ sr'' rr''] Jr''. move: (order_total_extension or'')=> [r''' [tr''' sr''' srr]]. move: (tr''') => [o3 _]. have aux: (inc r''' bs). apply: Zo_i; last by split => //;apply: sub_trans srr. by apply /ordersP;split => //; transitivity (substrate r''). move:(setI_hi tb aux) (srr _ Jr''); rewrite {1} tp => p3 p4. have pq: (P t = Q t) by order_tac. by rewrite tp pq;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)