proposition: Lemma greatest_is_setU s a: greatest (sub_order s) a -> a = union s.
proof: Proof. rewrite /greatest; move :(sub_osr s) => [_ ->] [asr h]. set_extens x => xs;first by union_tac. by move: (setU_hi xs)=> [y xy ys];move: (h _ ys) => /graph_on_P1 [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)