Shan_Problem_1_1 fails, need a `div n` of AngValue, need theorems concerning real as angle

[jjdishere]

Now angle/2 is not defined now. It is more convenient to define what is div n for all n. by first toReal then /n then toAngValue. However, this /n is bad at some calculation.

Further, we lost the ring tactic at calculation of angles, maybe it is easier to rewrite them as equalities of x.toReal the use ring?
Probably a better solution is to make theorems of real version derived from AngValue version. Then use real version theorems.

Should the notation \angle mean angvalue or real?