chore(topology/instances/add_circle): golf (#18020)
Net -23 lines. Also:
+ Switch the order of `exists_gcd_eq_one_of_is_of_fin_add_order` and `add_order_of_eq_pos_iff`.
+ Switch the order of `gcd_mul_add_order_of_div_eq` and `add_order_of_div_of_gcd_eq_one`.
+ Add easy lemmas `order_of_eq_iff`, `coe_period` and `add_order_of_period_div`.
+ Remove `[floor_ring]` hypothesis.
+ Replace `gcd` by `nat.gcd`.
Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
