proposition: Lemma orthocentre_ordre : forall A B C H : PO, triangle A B C -> H = orthocentre A B C :>PO -> H = orthocentre C A B :>PO.
proof: Proof. intros. elim orthocentre_def2 with (A := A) (B := B) (C := C) (H := H); [ intros | auto ]. elim H2; intros H4 H5; try clear H2; try exact H5. apply orthocentre_def; auto with geo. Qed.