proposition: Lemma orthocentre_triangle_rectangle : forall A B C : PO, triangle A B C -> orthogonal (vec A B) (vec B C) -> B = orthocentre A B C :>PO.
proof: Proof. intros. apply orthocentre_def; auto with geo. replace (vec B B) with zero; auto with geo. Ringvec. Qed.