proposition: Lemma existence_reflexion_AB : forall A B M : PO, A <> B -> exists M' : PO, M' = reflexion A B M.
proof: Proof. intros A B M H1; try assumption. elim existence_projete_orthogonal with (A := A) (B := B) (C := M); [ intros H H4; try clear existence_projete_orthogonal; try exact H3 | auto ]. elim existence_representant_vecteur with (A := H) (B := M) (C := H); intros M' H3; try clear existence_representant_vecteur; try exact H3. exists M'. apply reflexion_def2 with H; auto. replace (vec M M') with (add_PP (vec M H) (vec H M')). rewrite H3; Ringvec. Ringvec. Qed.