proposition: Lemma Cim_inv_compat_0 : forall z, Cim z = 0%R -> Cim (/z) = 0%R.
proof: Proof. intuition. destruct z. unfold Cinv. simpl in *. rewrite H. replace (- 0 / (r * r + 0 * 0))%R with (0%R). intuition. rewrite Ropp_0. unfold Rdiv. rewrite Rmult_0_l. reflexivity. Qed.
imports: Ctacfield Cbase Cpow Lia