proposition: Theorem reflexion_conjugaison : forall (z z' : C) (M M' : PO), z = affixe M -> z' = affixe M' -> M' = reflexion O I M -> z' = Conj z.
proof: Proof. intros z z' M M' H H0; try assumption. discrimine O M. cut (M <> I). intros H20. rewrite <- reflexion_axe; auto with geo. cut (z = zeroC); intros. rewrite H0; rewrite H3; rewrite <- H1; rewrite H2; auto. symmetry in |- *; rewrite <- affixe_origine; auto with geo. rewrite H; rewrite <- H1; auto with geo. rewrite <- H1; auto with geo. discrimine I M. rewrite <- reflexion_axe; auto with geo. cut (z = oneC); intros. rewrite H0; rewrite H4; rewrite <- H; rewrite H3; auto with geo. unfold oneC in |- *. apply cart_point_complexe with I. Ringvec. rewrite H; rewrite <- H2; auto. intros. cut (distance O M = distance O M'); intros. 2: apply (reflexion_isometrie (A:=O) (B:=I)); auto with geo. cut (cons_AV (vec O I) (vec O M') = opp (cons_AV (vec O I) (vec O M))); intros. 2: apply (reflexion_anti_deplacement (A:=O) (B:=I)); auto with geo. cut (O <> M'); intros. cut (z <> zeroC); intros. cut (z' <> zeroC); intros. apply egalite_forme_polaire; auto with geo. rewrite module_Conj. rewrite (module_def2 H); rewrite (module_def2 H0); auto. rewrite argument_Conj2; auto. rewrite (argument_def2 (M:=M) (z:=z)); auto with geo. rewrite (argument_def2 (M:=M') (z:=z')); auto with geo. eauto with geo. eauto with geo. apply isometrie_distinct with (2 := H4); auto with geo. Qed.