proposition: Lemma map_subseteq_size {A} (m1 m2 : M A) : m1 ⊆ m2 → size m1 ≤ size m2.
proof: Proof. intros. rewrite <-!map_to_list_length. by apply submseteq_length, map_to_list_submseteq. Qed.
imports: Coq(Permutation) stdpp(options)