proposition: Lemma select_diff : forall (P:set) (FP:finite P), (1 < size FP)%nat -> sigT (fun x => sigT (fun y => P x /\ P y /\ x<>y)).
proof: Proof. destruct FP; simpl; intros. absurd (1<0). auto with arith. apply H. exists x; destruct FP; simpl in H. absurd (1<1); auto with arith. exists x0; intuition. case (e x); auto. case (e0 x0); case (e x0); unfold add; intuition. subst; case (e0 x0); intuition. Qed.
imports: Coq(Arith) Coq(Lt)