Commit 2022-12-30 09:49 a437a249

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.