proposition: Lemma subset_size X Y : X ⊂ Y → size X < size Y.
proof: Proof. intros. rewrite (union_difference X Y) by set_solver. rewrite size_union_alt, difference_twice. cut (size (Y ∖ X) ≠ 0); [lia |]. by apply size_non_empty_iff, non_empty_difference. Qed.
imports: stdpp(relations) stdpp(options)