ROSCOQ.AngleMS

CR is an instance of CReals. But IR is not declared to be a Ring with order? There is something from CRing to ring_theory and ring_theory to Ring. We still need LT. CReals is is not defined for AQ. However, we can define it if we use AQ Since it really matters to make it fast on CR and not so much for CR, lets define it for CR and use CRasIR for IR? onenote:https://d.docs.live.net/946e75b47b19a3b5/Documents/PhD5/Submissions/ConHyb.one(computable)%20metric%20space%20on%20angles§ion-id={10FE6329-81C9-4025-AD71-4FC8EFC3BB57}&page-id={339A76CB-9539-4EAC-BF93-B3AD40D7818B}&end

first define subtraction which is supposed to be between -π and π? Either way, distance is supposed to be between 0 and π. It is a conitnuous function; implementable using min, max etc Distance of an angle from 0 radians. approximate it to some integel multiple of π/2 and then do induction on the integer