proposition: Lemma map_subset_size {A} (m1 m2 : M A) : m1 ⊂ m2 → size m1 < size m2.
proof: Proof. intros [Hm12 Hm21]. apply Nat.le_neq. split. - by apply map_subseteq_size. - intros Hsize. destruct Hm21. apply reflexive_eq, symmetry, map_subseteq_size_eq; auto with lia. Qed.
imports: Coq(Permutation) stdpp(options)