proposition: Lemma least_is_setI s a: least (sub_order s) a -> a = intersection s.
proof: Proof. rewrite /least;move: (sub_osr s) => [_ ->] [asr h]. set_extens x => xs; last by apply: setI_hi xs asr. apply: setI_i =>//; first by exists a. by move => y ys; move: (h _ ys) => /graph_on_P1 [_ _ ]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)