There is ```lean def ConstructibleAngle (θ : ℝ) : Prop := Constructible (Real.cos θ) ``` and ```lean def ConstructibleAngle (cfg : RCBase) (θ : ℝ) : Prop := ∃ P : Point, RCPoint cfg P ∧ baseAngle cfg P = θ ``` Is this causes some defination overload issue here?
There is
and
Is this causes some defination overload issue here?