proposition: Lemma Cre_div_compat : forall (z : C) (r : R), r <> R0 -> Cre (z / r) = (Cre z / r)%R.
proof: Proof. intros z r r_neq ; unfold Rdiv, Cdiv ; rewrite <- Cinv_IRC_Rinv ; [apply Cre_mult_compat_r | assumption]. Qed.
imports: Ctacfield Cbase Cpow Lia