proposition: Lemma finite_union : forall P Q, finite P -> finite Q -> finite (union P Q).
proof: Proof. intros P Q FP FQ; elim FP; intros. apply fin_equiv with Q; auto. apply equiv_trans with (union empty Q); auto. apply fin_equiv with (add x (union Q0 Q)); auto. apply equiv_trans with (union (add x Q0) Q); auto. apply fin_add_in; auto. Defined.
imports: Coq(Arith) Coq(Lt)