Similar triangles and orientation in plane elementary geometry for Coq-based proofs