proposition: Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq.
proof: Proof. constructor. - exact add_0_l. - exact add_comm. - exact add_assoc. - exact mul_1_l. - exact mul_comm. - exact mul_assoc. - exact mul_add_distr_r. - symmetry. apply add_opp_r. - exact add_opp_diag_r. Qed.
imports: ZArith Lia Znumtheory Zpow_facts DoubleType