proposition: Lemma i_carre : Csqr i = Rinj (-1).
proof: Proof. unfold Csqr in |- *. apply egalite_forme_polaire; auto with geo. rewrite Cmult_module; rewrite module_opp_un; rewrite module_i; ring. repeat rewrite Cmult_argument; auto with geo. rewrite argument_opp_un; rewrite argument_i. rewrite <- add_mes_compatible; auto. Qed.