proposition: Lemma aire_colinearite : forall (k : R) (A B C D : PO), vec C D = mult_PP k (vec A B) -> aire (vec A B) (vec C D) = 0.
proof: Proof. intros. discrimine A B. VReplace (vec B B) zero; auto with geo. discrimine C D. VReplace (vec D D) zero; auto with geo. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); [ intros E H2; try clear existence_representant_mult_vecteur; try exact H2 ]. replace (vec C D) with (vec A E). apply aire_alignement; auto. apply colineaire_alignes with k; auto. rewrite H; auto. Qed.