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