proposition: Lemma aire_anti_symetrique : forall A B C D : PO, aire (vec A B) (vec C D) = - aire (vec C D) (vec A B).
proof: Proof. intros. elim (classic (A = B \/ C = D)); intros. rewrite def_aire_0; auto. rewrite def_aire_0; auto. ring. tauto. cut (A <> B /\ C <> D); intros. elim H0; intros. rewrite def_aire; auto. rewrite def_aire; auto. rewrite Sin_opp; auto. ring. apply not_or_and; auto. Qed.