proposition: Lemma Cmult_eq_reg_l : forall z z1 z2 : C, z <> C0 -> z * z1 = z * z2 -> z1 = z2.
proof: Proof. intros z z1 z2 H0 H. assert (H1 : (/ z * z * z1 = z1)). rewrite Cinv_l . apply Cmult_1_l . exact H0. assert (H2 : (/ z * z * z2 = z2)). rewrite Cinv_l . apply Cmult_1_l . exact H0. rewrite <- H1. rewrite Cmult_assoc. rewrite H. rewrite <- Cmult_assoc; apply H2. Qed.
imports: Ctacfield Cbase Cpow Lia