proposition: Lemma reflexion_projete_orthogonal_milieu : forall A B M M' H : PO, A <> B -> H = projete_orthogonal A B M -> M' = reflexion A B M -> H = milieu M M'.
proof: Proof. intros. generalize (reflexion_def (A:=A) (B:=B) (M:=M) (M':=M') (H:=H)); intros H5. cut (2 <> 0); intros. apply vecteur_milieu. rewrite H5; auto. replace (mult_PP (/ 2) (mult_PP 2 (vec M H))) with (mult_PP (/ 2 * 2) (vec M H)). replace (/ 2 * 2) with 1. Ringvec. auto with real. Ringvec. discrR. Qed.