proposition: Lemma infinite_rem a P : infinite (rem a P) <-> infinite P.
proof: Proof. unfold infinite. gen (finite_rem_eq a P). tauto. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)