proposition: Lemma aire_colineaire_r : forall (k : R) (A B C D : PO), aire (vec A B) (mult_PP k (vec C D)) = k * aire (vec A B) (vec C D).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := C) (C := D) (k := k); [ intros E H2; rewrite <- H2 ]. rewrite aire_anti_symetrique. rewrite H2; rewrite aire_colineaire_l; auto. rewrite aire_anti_symetrique; ring. Qed.