proposition: Theorem conjugaison_reflexion : forall (z : C) (M M' : PO), z = affixe M -> Conj z = affixe M' -> M' = reflexion O I M.
proof: Proof. intros z M M'; try assumption. discrimine O M. cut (M <> I); intros. rewrite <- reflexion_axe; auto with geo. cut (z = zeroC); intros. apply egalite_affixe_point with (1 := H2) (2 := H1); auto. rewrite H3; auto with geo. rewrite H1; rewrite <- H; auto with geo. rewrite <- H; auto with geo. elim (classic (alignes O I M)); intros. rewrite <- reflexion_axe; auto with geo. apply egalite_affixe_point with (1 := H2) (2 := H1); auto. halignes H0 k. absurd (O = I); auto with geo. cut (z = cons_cart k 0); intros. 2: apply cart_point_complexe with M; auto. rewrite H4; rewrite Conj_algebrique. replace (-0) with 0; [ auto | ring ]. rewrite H3; Ringvec. elim existence_projete_orthogonal with (A := O) (B := I) (C := M); [ intros N H4; try clear existence_projete_orthogonal; try exact H4 | auto with geo ]. apply reflexion_def2 with N; auto with geo. elim existence_parties_relles_imaginaires with (z := z); intros a H6; elim H6; intros b H7; try clear H6 existence_parties_relles_imaginaires; try exact H7. cut (Rinj a = affixe N); intros. apply produit_reel_affixe_vecteur with (z := Cplus (Rinj a) (Copp z)) (z' := Cplus (Conj z) (Copp z)); auto with geo. unfold Rinj in |- *. rewrite H7; rewrite Conj_algebrique. rewrite Copp_algebrique; repeat rewrite Cplus_algebrique. rewrite Cmult_algebrique. replace (2 * (a + - a) + - (0 * (0 + - b))) with (a + - a); [ auto | ring ]. replace (0 * (a + - a) + 2 * (0 + - b)) with (- b + - b); [ auto | ring ]. apply (affixe_projete_orthogonal (z:=z) (a:=a) (b:=b) (M:=M) (H:=N)); auto. Qed.