proposition: Lemma finite_remove_inv : forall E F, finite (E \- F) -> finite F -> finite E.
proof: Proof. Proof using. introv H1 H2. lets (L1&R1): finite_inv_list_covers H1. lets (L2&R2): finite_inv_list_covers H2. applys finite_of_list_covers (L1 ++ L2). intros y Hy. rewrite~ mem_app_eq. tests: (y \in F). autos~. forwards~ M: R1 y. rewrite~ @in_remove_eq. typeclass. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)