proposition: Lemma vec_OAplusOBplusOC_orthogonal : forall A B C A' O M : PO, A' = milieu B C -> circonscrit O A B C -> vec O M = add_PP (vec O A) (add_PP (vec O B) (vec O C)) -> orthogonal (vec A M) (vec B C).
proof: Proof. intros. cut (orthogonal (vec O A') (vec B C)); intros. replace (vec A M) with (add_PP (mult_PP (-1) (vec O A)) (vec O M)); [ idtac | Ringvec ]. replace (add_PP (mult_PP (-1) (vec O A)) (vec O M)) with (add_PP (vec O B) (vec O C)). rewrite (prop_vecteur_milieu (B:=B) (C:=C) (A':=A') O); auto with geo. rewrite H1; Ringvec. apply milieu_centrecirconscrit_orthogonal_segment with A; auto. Qed.