Commit 2022-08-10 15:00 ce9af07f

feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966) Previously I had use for the operation of reducing a real number to an interval modulo the length of that interval, in proving results about complex.arg, and as it was only being used in one place, inlined expressions in terms of int.fract and associated proofs where needed. Now I'd like to make further use of that operation, so define actual functions to reduce to an interval (Ico or Ioc, in an archimedean linear_ordered_add_comm_group) and set up associated API for those definitions. In the case of a linear_ordered_field that is a floor_ring, these definitions are proved equal to explicit expressions in terms of fract and floor. Previous uses for complex.arg are updated to illustrate the use of the new API.