proposition: Lemma Exercise2_7c: least (closure_ordering) (identity (substrate r)).
proof: Proof. have ifsr: inc (identity E) closures. apply: Zo_i ;first by apply /functionsP;red;aw;split;fprops. split => //. - split => //; first by apply: identity_prop. move=> x y xy; rewrite ! idV//; rewrite /E;order_tac. - by move=> x xsr; rewrite idV//; order_tac. - move => x xsr; rewrite ! idV//. move: Exercise2_7b => [p1 p2]. red; rewrite p2;split => // x xs; apply /Exercise2_7aP; split => //. move => i isr; rewrite idV//. by move: xs => /Zo_hi [_ p4 _];apply: p4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)