proposition: Lemma triangle_distincts_pied_hauteur : forall A B C H : PO, triangle A B C -> H = projete_orthogonal A B C -> C <> H :>PO.
proof: Proof. intros. deroule_triangle A B C. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. red in |- *; intros; apply H2. rewrite H8; auto. Qed.