proposition: Lemma Exercise2_7B5 : has_greatest r -> has_greatest (closure_ordering).
proof: Proof. move => [a [asr age]]. have ha: cofinal r (singleton a). split; [ by move =>t /set1_P-> | move => x xsr; ex_tac]. have hb: worder (induced_order r (singleton a)). move: (iorder_osr or (set1_sub asr)) => hb. apply: (worder_set1 hb). move: (Exercise2_7B2 ha hb) =>[u uc etc]. exists u => //; split; rewrite (proj2 Exercise2_7b) => // v vc. apply/ (Exercise2_7dP vc uc); rewrite etc => t /set1_P ->. move: vc =>/Zo_P[/functionsP[ff sf tf] [qa qb qc]]. apply/Zo_P; rewrite sf; split => //. move: (qb _ asr) => h1. move: (age _ (arg2_sr h1))=> h2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)