proposition: Lemma Cmult_eq_reg_r : forall z z1 z2 : C, z <> C0 -> z1 * z = z2 * z -> z1 = z2.
proof: Proof. intros z z1 z2 H H1. apply Cmult_eq_reg_l with z. exact H. rewrite Cmult_comm ; rewrite H1 ; apply Cmult_comm. Qed.
imports: Ctacfield Cbase Cpow Lia