proposition: Lemma Cinv_neq_0_compat : forall z : C, z <> C0 -> / z <> C0.
proof: Proof. intros z H. intro H0. apply (Cmult_eq_0_compat_l z) in H0. apply Cinv_r in H. rewrite H in H0. apply C1_neq_C0 ; exact H0. Qed.
imports: Ctacfield Cbase Cpow Lia