proposition: Lemma aire_avec_projete : forall A B C H : PO, A <> B -> H = projete_orthogonal A B C -> aire (vec A B) (vec A C) = aire (vec A B) (vec H C).
proof: Proof. intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. VReplace (vec A C) (add_PP (vec A H) (vec H C)). repeat rewrite aire_distrib_l. rewrite aire_alignement; auto. ring. Qed.