proposition: Lemma aire_AB_oppAB : forall A B C : PO, aire (vec A B) (mult_PP (-1) (vec A B)) = 0.
proof: Proof. intros. elim (existence_representant_mult_vecteur A A B (-1)); auto; intros D H. rewrite <- H. elim (classic (A = B)); intros. rewrite def_aire_0; auto. cut (A <> D); intros. rewrite def_aire; auto. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=D) (x:=pi)); auto. rewrite sin_pi; ring. replace (vec A D) with (vec B A). apply angle_plat; auto. rewrite H; Ringvec. apply distinct_produit_vecteur with (3 := H); auto with real. Qed.