proposition: Lemma Exercise2_7b: order_on closure_ordering closures.
proof: Proof. rewrite /closure_ordering. move: (order_function_osr E or (refl_equal E)) => [p1 p2]. apply:iorder_osr => //; rewrite p2; apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)