proposition: Lemma determinant_aire : forall A B C D : PO, det (vec A B) (vec C D) = aire (vec A B) (vec C D).
proof: Proof. intros. elim composantes_vecteur with (O := O) (I := I) (J := J) (M := A) (N := B); [ intros x H; elim H; [ intros y H0; try clear H composantes_vecteur; try exact H0 ] | auto with geo ]. elim composantes_vecteur with (O := O) (I := I) (J := J) (M := C) (N := D); [ intros x' H1; elim H1; [ intros y' H2; try clear H1 composantes_vecteur; try exact H2 ] | auto with geo ]. rewrite (determinant_def (A:=A) (B:=B) (C:=C) (D:=D) (x:=x) (y:=y) (x':=x') (y':=y')) ; auto. generalize H0 H2. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros E H3; rewrite <- H3 ]. elim existence_representant_vecteur with (A := O) (B := C) (C := D); [ intros F H4; rewrite <- H4 ]. intros; symmetry in |- *. apply aire_coordonnees; auto. Qed.