proposition: Lemma aire_ABAB : forall A B : PO, aire (vec A B) (vec A B) = 0.
proof: Proof. intros. elim (classic (A = B)); intros. rewrite def_aire_0; auto. rewrite def_aire; auto. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=B) (x:=0)); auto. rewrite sin_zero; ring. apply angle_nul; auto. Qed.