proposition: Lemma setIrel_or z: (alls z order) -> order (intersection z).
proof: Proof. move=> alleq;split. - by apply: setIrel_graph => r /alleq []. - by apply: setIrelR => r /alleq [_ ]. - by apply: setIrelT=> // r /alleq [_ _ ]. - case: (emptyset_dichot z). move => ->; rewrite setI_0 => a b; case; case. move => [t te] x y pa pb; move: (alleq _ te)=> [_ _ _]; apply. apply:(setI_hi pa te). apply:(setI_hi pb te). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)