Formalization of the theory of oriented angles of non zero vectors using Coq is reported. Using this theory, some classical plane geometry theorems are proved, among them : the theorem which gives a necessary and sufficient condition so that four points are cocyclic, the one which shows that the reflected points with respect to the sides of a triangle orthocenter are on its circumscribed circle, the Simson's theorem and the Napoleon's theorem. Elaboration of proofs using Coq that followed the traditional proofs in geometry, and the difficulties encountered are described. Use of the interface Pcoq allows notations close to mathematical ones.