proposition: Lemma projete_sinus : forall (x : R) (A B C H : PO), A <> B -> A <> C -> H = projete_orthogonal A B C -> image_angle x = cons_AV (vec A B) (vec A C) -> distance H C = distance A C * Rabs (sin x).
proof: Proof. intros. rewrite (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto. rewrite (projete_Sinus (A:=A) (B:=B) (C:=C) (H:=H)); auto. Qed.