proposition: Lemma projete_absolu_Sin : forall A B C H : PO, triangle A B C -> H = projete_orthogonal A B C -> distance C H = distance C A * Rabs (Sin (cons_AV (vec A B) (vec A C))).
proof: Proof. intros. deroule_triangle A B C. mes (cons_AV (vec A B) (vec A C)). rewrite <- H6. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto. apply projete_absolu_sin with B; auto. Qed.