proposition: Lemma projete_absolu_Cos : forall A B C H : PO, A <> B -> A <> C -> H = projete_orthogonal A B C -> distance A H = distance A C * Rabs (Cos (cons_AV (vec A B) (vec A C))).
proof: Proof. intros. mes (cons_AV (vec A B) (vec A C)). rewrite <- H3. rewrite <- (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=x)); auto. apply projete_absolu_cos with B; auto. Qed.