proposition: Lemma aire_orthogonal : forall A B C D : PO, orthogonal (vec A B) (vec C D) -> Rabs (aire (vec A B) (vec C D)) = distance A B * distance C D.
proof: Proof. intros. discrimine A B. VReplace (vec B B) zero; auto with geo. rewrite aire_vecteur_nul_l; rewrite Rabs_R0. replace (distance B B) with 0; [ring|idtac]. symmetry in |- *; auto with geo. discrimine C D. VReplace (vec D D) zero; auto with geo. rewrite aire_vecteur_nul_r; rewrite Rabs_R0. replace (distance D D) with 0; [ring|idtac]. symmetry in |- *; auto with geo. elim orthogonal_pisurdeux_or with (A := A) (B := B) (C := C) (D := D); [ intros H2; try clear orthogonal_pisurdeux_or | intros H2; try clear orthogonal_pisurdeux_or; try exact H2 | auto | auto | auto ]. rewrite aire_orthogonal_direct; auto. rewrite Rabs_mult; rewrite Rabs_right; auto with geo. rewrite Rabs_right; auto with geo. rewrite aire_orthogonal_indirect; auto. rewrite Rabs_Ropp; rewrite Rabs_mult; rewrite Rabs_right; auto with geo. rewrite Rabs_right; auto with geo. Qed.