proposition: Lemma vec_OAplusOBplusOC_orthocentre : forall A B C O M : PO, triangle A B C -> circonscrit O A B C -> vec O M = add_PP (vec O A) (add_PP (vec O B) (vec O C)) -> M = orthocentre A B C.
proof: Proof. intros. deroule_triangle A B C. soit_milieu B C A'. lapply (vec_OAplusOBplusOC_orthogonal (A:=A) (B:=B) (C:=C) (A':=A') (O:=O) (M:=M)); intros; auto. cut (orthogonal (vec C M) (vec A B)); intros. cut (orthogonal (vec B M) (vec C A)); intros. apply orthocentre_def; auto with geo. cut (orthogonal (vec A M) (vec B C)); intros; auto with geo. soit_milieu A C B'. apply (vec_OAplusOBplusOC_orthogonal (A:=B) (B:=C) (C:=A) (A':=B') (O:=O) (M:=M)); auto with geo. apply circonscrit_permute; auto. apply circonscrit_permute; auto. rewrite H1; Ringvec. soit_milieu A B C'. apply (vec_OAplusOBplusOC_orthogonal (A:=C) (B:=A) (C:=B) (A':=C') (O:=O) (M:=M)); auto. apply circonscrit_permute; auto. rewrite H1; Ringvec. Qed.