proposition: Lemma reflexion_symetrie : forall A B M M' : PO, A <> B -> M' = reflexion A B M -> M = reflexion A B M'.
proof: Proof. intros A B M M' H1 H0; try assumption. elim (classic (alignes A B M)); intros H20. rewrite H0. rewrite <- reflexion_axe. rewrite <- reflexion_axe; auto. auto. rewrite <- reflexion_axe; auto. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H3; try clear existence_projete_orthogonal; try exact H3 | auto ]. generalize (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros H5. generalize (reflexion_projete_orthogonal_milieu (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. generalize (projete_orthogonal_image (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros. generalize (non_axe_image_non_axe (A:=A) (B:=B) (M:=M) (M':=M')); intros. apply reflexion_def2 with H; auto with geo. Qed.