proposition: Lemma Cinv_Conj : forall z : C, z <> zeroC -> Cinv z = Cmult (Cinv (Rinj (Rsqr (module z)))) (Conj z).
proof: Proof. intros. assert (module z <> 0); auto with geo. assert (Rsqr (module z) <> 0). unfold Rsqr in |- *; auto with real. assert (Rinj (Rsqr (module z)) <> zeroC); auto with geo. assert (Cmult z (Cmult (Cinv (Rinj (Rsqr (module z)))) (Conj z)) = oneC). 2: apply Cinv_def2; auto. replace (Cmult z (Cmult (Cinv (Rinj (Rsqr (module z)))) (Conj z))) with (Cmult (Cinv (Rinj (Rsqr (module z)))) (Cmult z (Conj z))). rewrite produit_Conj_module. apply Cinv_l; auto. ring. Qed.