proposition: Lemma projete_Sinus : forall A B C H : PO, A <> B -> A <> C -> H = projete_orthogonal A B C -> distance H C = distance A C * Rabs (Sin (cons_AV (vec A B) (vec A C))).
proof: Proof. intros. apply Rmult_eq_reg_l with (distance A B); auto with geo. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. rewrite <- aire_orthogonal; auto. rewrite <- aire_avec_projete; auto. rewrite def_aire; auto. rewrite Rabs_mult; rewrite Rabs_right; auto with geo. rewrite Rabs_mult; rewrite Rabs_right; auto with geo. Qed.