AngValue should copy all api's of Real.Angle that could be used in future in the file Basic.Angle #233
Description
AngValue should copy all api's that could be used in future in the file Basic.Angle.
Also those used Real.Angle such as theorems mentioned sin cos,....
Another solution is to use abbrev, it works well with simp, dot, but to use a theorem of Angle, the name is still written as Real.Angle.xxx or Angle.xxx if we export.