Proofs Section 1.1 (Initial results to LF-duality) — LessWrong