proposition: Lemma size_incl : forall (P:set)(f:finite P) (Q:set)(g:finite Q), (incl P Q)-> size f <= size g.
proof: Proof. induction f; simpl; intros; auto with arith. apply le_trans with (S (size (finite_rem x g))). apply le_n_S. apply IHf with (g:= finite_rem x g); auto. apply incl_trans with (rem x P); auto. apply incl_add_rem; auto. apply incl_rem_stable; auto. rewrite <- size_finite_rem; auto. case (e x); intuition. Qed.
imports: Coq(Arith) Coq(Lt)