proposition: Lemma Conj_Cdiv : forall z z' : C, z' <> zeroC -> Conj (Cdiv z z') = Cdiv (Conj z) (Conj z').
proof: Proof. intros. rewrite Cdiv_def; auto; rewrite Conj_produit; rewrite Conj_Cinv; auto. rewrite <- Cdiv_def; auto with geo. Qed.