proposition: Lemma orthocentre_double : forall A B C H : PO, H <> B :>PO -> H <> C :>PO -> triangle A B C -> H = orthocentre A B C :>PO -> double_AV (cons_AV (vec H C) (vec H B)) = double_AV (cons_AV (vec A B) (vec A C)) :>AV.
proof: Proof. intros. elim orthocentre_def2 with (A := A) (B := B) (C := C) (H := H); [ intros | auto ]. elim H4; intros H6 H7; try clear H4; try exact H7. deroule_triangle A B C. apply angles_droites_orthogonales; auto with geo. Qed.