proposition: Lemma Exercise2_1bP E r: maximal (finer_order E) r <-> (total_order r /\ substrate r = E).
proof: Proof. rewrite /maximal (proj2 (fo_osr _)); split. move=> [] /ordersP [oa sa] ha; split => //; split =>//. move=> x y xsr ysr; case: (p_or_not_p (gle r y x)) => ngge; first by right. by left; case(Exercise2_1a oa xsr ysr ngge); rewrite sa; move/ha ->. move=> [[oa ta] sa]; split => //; first by apply /ordersP;split => //. move=> x /fo_gle1P [_ ox _ sx sv]. symmetry; apply: order_exten => // u v;split => h. apply: sv =>//; rewrite - sa; order_tac. move:(arg1_sr h)(arg2_sr h); rewrite sx => usr vsr. rewrite sa in ta; case: (ta _ _ usr vsr) => //. move => uv; move: (sv _ _ vsr usr uv) => h'. move: uv; have -> //: u = v by order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)