proposition: Lemma size_delete `{EqDec k} i m : (size (delete i m) <= size m)%nat.
proof: Proof. induction m; simpl; auto. destruct (eq_dec i k0) eqn:Heqe; auto; simpl; lia. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib