proposition: Lemma aire_distrib_r : forall A B C D E F : PO, aire (add_PP (vec A B) (vec C D)) (vec E F) = aire (vec A B) (vec E F) + aire (vec C D) (vec E F).
proof: Proof. intros. replace (aire (vec A B) (vec E F) + aire (vec C D) (vec E F)) with (- (aire (vec E F) (vec A B) + aire (vec E F) (vec C D))). rewrite <- aire_distrib_l. elim existence_representant_som_vecteur with (A := A) (B := B) (C := C) (D := D); [ intros G H2; rewrite <- H2 ]. auto with geo. rewrite aire_anti_symetrique. rewrite (aire_anti_symetrique E F C D); ring. Qed.