proposition: Lemma aire_orthogonal_indirect : forall A B C D : PO, A <> B -> C <> D -> image_angle (- pisurdeux) = cons_AV (vec A B) (vec C D) -> aire (vec A B) (vec C D) = - (distance A B * distance C D).
proof: Proof. intros A B C D H H0; try assumption. elim existence_representant_vecteur with (A := A) (B := C) (C := D); [ intros E H2; rewrite <- H2; intros ]. rewrite def_aire; auto. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=E) (x:=- pisurdeux)); auto with geo. replace (distance C D) with (distance A E); auto with geo. rewrite sin_impaire; rewrite sin_pisurdeux; ring. apply distinct_egalite_vecteur with (2 := H2); auto with geo. apply distinct_egalite_vecteur with (2 := H2); auto with geo. Qed.