proposition: Lemma setI_least s: inc (intersection s) s -> least (sub_order s) (intersection s) .
proof: Proof. move=> iis;hnf; rewrite (proj2 (sub_osr s)); split => //. by move => x xs;apply/graph_on_P1;split => //; apply: setI_s1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)