proposition: Lemma Conj_Cinv : forall z : C, z <> zeroC -> Conj (Cinv z) = Cinv (Conj z).
proof: Proof. intros. cut (Cmult z (Cinv z) = oneC); (intros; auto with geo). cut (Cmult (Conj z) (Conj (Cinv z)) = oneC); intros. cut (Cinv (Conj z) = Conj (Cinv z)); intros. 2: apply Cinv_def2; auto with geo. rewrite <- H2; auto with geo. rewrite <- Conj_produit; rewrite H0; auto with geo. Qed.