proposition: Lemma unicite_inverse : forall z z1 z2 : C, z <> zeroC -> Cmult z z1 = oneC -> Cmult z z2 = oneC -> z1 = z2.
proof: Proof. intros. cut (module z * module z1 = 1); intros. cut (module z * module z2 = 1); intros. cut (module z <> 0); intros; auto with geo. cut (module z1 <> 0); intros. cut (module z2 <> 0); intros. cut (z1 <> zeroC); intros; auto with geo. cut (z2 <> zeroC); intros; auto with geo. apply egalite_forme_polaire; auto with geo. replace (module z1) with (/ module z); auto with real. auto with real. cut (plus (argument z) (argument z1) = image_angle 0); intros. cut (plus (argument z) (argument z2) = image_angle 0); intros. rewrite (opp_angle (a:=argument z) (b:=argument z1)); auto. rewrite (opp_angle (a:=argument z) (b:=argument z2)); auto. rewrite <- Cmult_argument; auto with geo. rewrite H1; rewrite <- argument_oneC; auto. rewrite <- Cmult_argument; auto with geo. rewrite H0; rewrite <- argument_oneC; auto. cut (module z * module z2 <> 0); intros. red in |- *; intros; apply H6. rewrite H7; ring. rewrite H3; discrR. cut (module z * module z1 <> 0); intros. red in |- *; intros; apply H5. rewrite H6; ring. rewrite H2; discrR. rewrite <- Cmult_module; rewrite H1; rewrite <- module_oneC; auto. rewrite <- Cmult_module; rewrite H0; rewrite <- module_oneC; auto. Qed.