Formal Analysis of Geometrical Optics using Theorem Proving