proposition: Lemma set0_wor: worder_on emptyset emptyset.
proof: Proof. move:set0_osr => [oe se]. split=> //; split => //; rewrite se; move => x xs [y yx]. case: (in_set0 (xs _ yx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)