proposition: Lemma deux_hauteurs_trois : forall A B C H : PO, orthogonal (vec H A) (vec B C) -> orthogonal (vec H B) (vec A C) -> orthogonal (vec H C) (vec A B).
proof: Proof. intros. apply def_orthogonal2. replace (vec H C) with (add_PP (vec H A) (vec A C)) by Ringvec. lapply (def_orthogonal (A:=H) (B:=A) (C:=B) (D:=C)); auto; intros. lapply (def_orthogonal (A:=H) (B:=B) (C:=A) (D:=C)); auto; intros. Simplscal. replace (scalaire (vec H A) (vec A B)) with (scalaire (vec H A) (vec A C)). replace (scalaire (vec H A) (vec A C) + scalaire (vec A C) (vec A B)) with (scalaire (add_PP (vec H A) (vec A B)) (vec A C)). replace (add_PP (vec H A) (vec A B)) with (vec H B); auto. Ringvec. Simplscal. rewrite (scalaire_sym A B A C); auto. replace (vec A B) with (add_PP (vec A C) (vec C B)). Simplscal. replace (vec C B) with (mult_PP (-1) (vec B C)). Simplscal. rewrite H2; ring. Ringvec. Ringvec. Qed.