proposition: Lemma aire_triangle_projete : forall A B C H : PO, A <> B -> H = projete_orthogonal A B C -> aire_triangle A B C = / 2 * (distance A B * distance H C).
proof: Proof. unfold aire_triangle in |- *; intros. discrimine A C. assert (H = A). rewrite <- H2 in H1. apply projete_axe with (2 := H1); auto with geo. assert (H = C). rewrite H3; auto. assert (distance H C = 0); auto with geo. rewrite H5. rewrite def_aire_0. rewrite Rabs_right; auto with real. right; auto. rewrite def_aire; auto. rewrite (projete_Sinus (A:=A) (B:=B) (C:=C) (H:=H)); auto. rewrite Rabs_mult. rewrite Rabs_mult. rewrite (Rabs_right (distance A B)); auto with geo. rewrite (Rabs_right (distance A C)); auto with geo. Qed.