proposition: Lemma infinite_union P Q : infinite (union P Q) <-> infinite P \/ infinite Q.
proof: Proof. unfold infinite. gen (finite_union_eq P Q). tauto. Qed.
imports: Coq(Basics Morphisms Setoid Lia) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil SetUtil FinSet FunUtil BoundNat IotaUtil EpsilonUtil)