proposition: Lemma reflexion_axe : forall A B M : PO, A <> B -> alignes A B M -> M = reflexion A B M.
proof: Proof. intros A B M H2 H0; try assumption. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H3; try clear existence_projete_orthogonal; try exact H3 | auto ]. apply reflexion_def2 with H; auto. cut (M = H); intros. rewrite <- H1; Ringvec. rewrite H3. apply def_projete_orthogonal; auto. replace (vec M M) with zero; auto with geo. Ringvec. Qed.