Library GeoCoq.Meta_theory.Parallel_postulates.rah_rectangle_principle