proposition: Lemma Exercise2_7aP f g: gle (closure_ordering) f g <-> [/\ inc f (closures), inc g (closures) & forall i, inc i (substrate r) -> gle r (Vf f i) (Vf g i)].
proof: Proof. move: (order_function_osr E or (refl_equal E)) => [or' sr']. have p1: (sub (closures) (substrate (order_function E E r))). rewrite sr'; apply: Zo_S. rewrite /closure_ordering; split => h. move: (iorder_gle1 h)(iorder_gle3 h) => fg [fs gs]; split => //. by move: fg => /order_functionP [_ _ ok]. move: h => [h1 h2 h3];apply/iorder_gle0P => //. by move: h1 h2 => /Zo_P [h1 h2] /Zo_P [h3' h4]; apply /order_functionP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)