namespace http://mathhub.info/MitM/core/geometry ❚

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
// TODO: ❚
import rules scala://rules.frameit.mmt.kwarc.info ❚

fixmeta base:?Logic ❚

theory PlanarGeometry =
  include ☞base:?ProductTypes ❙
  include ?Geometry ❙

  // ℝ² ❙

  point = ℝ × ℝ ❙
  xofpoint : point ⟶ ℝ ❘ = [p] πl p ❘ # 1 _x prec 50 ❙
  yofpoint : point ⟶ ℝ ❘ = [p] πr p ❘ # 1 _y prec 50 ❙

  point_addI = [p1,p2] ⟨ (p1 _x + p2 _x), (p1 _y + p2 _y) ⟩ ❙
  point_subtractI = [p1,p2] ⟨ (p1 _x - p2 _x), (p1 _y - p2 _y) ⟩ ❙
  vec_multI = [r,p] ⟨ r ⋅ p _x, r ⋅ p _y ⟩ ❙
  scalar_productI = [p1,p2] (p1 _x ⋅ p2 _x) + (p1 _y ⋅ p2 _y) ❙

  include (?Geometry/Common point point_addI point_subtractI vec_multI scalar_productI) ❙
❚