proposition: Lemma set0_osr: order_on emptyset emptyset.
proof: Proof. split; first by rewrite - setI_0; apply: setIrel_or => t /in_set0. by rewrite /substrate domain_set0 range_set0 setU2_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)