proposition: Lemma size_compress `{EqDec k} m : (size (compress m) <= size m)%nat.
proof: Proof. induction m; auto. simp compress; simpl. apply le_n_S. rewrite compress_delete. now rewrite size_delete. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib