The Linea Prover Explained