proposition: Lemma determinant_aire_triangle : forall A B C : PO, aire_triangle A B C = / 2 * Rabs (det (vec A B) (vec A C)).
proof: Proof. unfold aire_triangle in |- *; intros. repeat rewrite determinant_aire; auto. Qed.