An important theoretical observation behind Coq is the Curry-Howard correspondence, which states that types and logical formulas are fundamentally the same thing, and so are programs and proofs. The intuition is that a proof is a program that constructs an object of the desired type; a formula is true if there is a way to construct a proof of it, i.e. the corresponding type is not empty. In this correspondence, applying a function is the modus ponens rule.
When you prove a theorem in Coq, Coq constructs a proof term behind the scenes. However, you state the proof in Coq's proof language, by stating a sequence of tactics to apply. Executing these tactics builds a term, which Coq typechecks when you write Qed; if the term has the desired type, i.e. proves the desired formula, then Coq accepts the proof. (The tactic language is constructed so that most tactic sequences form a valid proof when all subgoals are fulfilled, but this can be bypassed.)
You can terminate a proof with Defined instead of Qed. If you do that, the proof term is transparent, which means that you can make use of how the theorem has been proved. With Qed, the proof is opaque, so you know that the theorem holds, but you can't rely on its having any particular proof.
Knowing the way a theorem is proved is rarely useful. But theorems are the same as types; knowing a way to build a value of a type is often useful — the difference between + and * (both of type nat -> nat -> nat) is very often relevant. So ending a theorem with Defined is a way to define a term; if you do that, you might as well use the keyword Definition rather than Theorem or Lemma (and in fact the syntax treats these keywords as equivalent).
The reason one would use tactics rather than write out a proof term is that terms with heavily dependent types can be hard to write manually. Often, these terms are what you'd think of as data structures or functions building data structures with bits of proofs embedded in them. Since all Coq guarantees that you're building a term of the right type, you'd better carefully review the tactics when you do this, as it's easy to accidentally build a term which is not what you intended. The Program facility (which is more recent than the ZFC library) makes it easier to write such programs with embedded bits of proofs: you write the program bits as terms, and then complete the proof bits with tactics.
