existential quantifier: how to refer to the instance

Question

I have a theorem in which I show that an object exists that satisfies some property. I proved this theorem by constructing the object. Then, in another proof, I would like to refer to the object defined in the first theorem in the statement of the second theorem. I know the object should be accessible if I close my proof with Defined rather than Qed, but I don't know how to access it. For example:

Theorem T1: exists x, P x. Proof. ... Defined.

Theorem T2: for the same x constructed in T1, Q x \/ R x. Proof. ... Qed.

How do I express this in Coq?

Answer 1

In this case, you should simply define the object (x) using a definition.

Definition object : (...) := 
  ...

Theorem T1 : exists x, P x.
  Proof.
  exists object.
    ...
  Qed.

Theorem T2 : ...

where the proof of T2 uses this same object. You may find that certain tactics (namely, exact, doubly so if this is something that lives in Prop) will help you here as they let you manipulate raw proof objects more easily.