proposition: Lemma aire_ordre_cycle : forall A B C : PO, aire (vec B C) (vec B A) = aire (vec A B) (vec A C).
proof: Proof. intros. VReplace (vec B C) (add_PP (vec B A) (vec A C)). rewrite aire_distrib_r; rewrite aire_ABAB; ring_simplify. VReplace (vec B A) (mult_PP (-1) (vec A B)). rewrite aire_colineaire_r; rewrite aire_anti_symetrique; ring. Qed.