proposition: Lemma aire_nulle_colineaires : forall A B C D : PO, A <> B -> aire (vec A B) (vec C D) = 0 -> exists k : R, vec C D = mult_PP k (vec A B).
proof: Proof. intros. discrimine C D. exists 0. Ringvec. cut (Sin (cons_AV (vec A B) (vec C D)) = 0); intros. deroule_representant_unitaire A B E. deroule_representant_unitaire C D J. elim existence_representant_vecteur with (A := A) (B := C) (C := J); [ intros F H14; intros ]. elim existence_ROND_AB with (A := A) (B := E); [ intros G H13 | auto with geo ]. cut (vec A F = add_PP (mult_PP (Cos (cons_AV (vec A E) (vec A F))) (vec A E)) (mult_PP (Sin (cons_AV (vec A E) (vec A F))) (vec A G))); intros. halignes H4 k. assert (alignes C J D); auto with geo. halignes H17 k'. cut (Sin (cons_AV (vec A E) (vec A F)) = 0); intros. rewrite H18; rewrite <- H14; rewrite H15. pattern (vec A E) at 2 in |- *; rewrite H16; rewrite H19. exists (k' * (Cos (cons_AV (vec A E) (vec A F)) * k)). Ringvec. rewrite <- H2. rewrite H14. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. rewrite H8; rewrite H3. rewrite representant_unitaire_bis; auto. rewrite representant_unitaire_bis; auto. apply coordonnees_Cos_Sin; auto. apply carre_scalaire_1_distance. rewrite H14; auto. replace (Sin (cons_AV (vec A B) (vec C D))) with (aire (vec A B) (vec C D) * / (distance A B * distance C D)). rewrite H0; ring. rewrite def_aire; auto. field; auto with geo. Qed.