proposition: Lemma aire_alignement : forall A B C : PO, alignes A B C -> aire (vec A B) (vec A C) = 0.
proof: Proof. intros. discrimine A B. VReplace (vec B B) zero; auto with geo. discrimine A C. VReplace (vec C C) zero; auto with geo. rewrite def_aire; auto. rewrite Sin_angles_alignes; auto. ring. Qed.