the Lemma command simply mutates the current state to push a new proof obligation to the top of the stack of things you must prove
Proof. and Qed. do nothing at all but they're similar to how math proofs are written so they're useful for human legibility