proposition: Lemma set_subseteq_size_equiv X1 X2 : X1 ⊆ X2 → size X2 ≤ size X1 → X1 ≡ X2.
proof: Proof. intros. apply (anti_symm _); [done|]. apply empty_difference_subseteq, size_empty_iff. rewrite size_difference by done. lia. Qed.
imports: stdpp(relations) stdpp(options)