proposition: Lemma angle_pi_negatif_colineaire : forall A B C : PO, A <> B -> A <> C -> cons_AV (vec A B) (vec A C) = image_angle pi -> exists k : R, k < 0 /\ vec A C = mult_PP k (vec A B).
proof: Proof. intros A B C H H0; try assumption. cut (cons_AV (vec A B) (vec A C) = cons_AV (representant_unitaire (vec A B)) (representant_unitaire (vec A C))); auto with geo. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H3; try clear existence_representant_unitaire; rewrite <- H3 | auto ]. elim existence_representant_unitaire with (A := A) (B := C); [ intros C' H4; rewrite <- H4 | auto ]. intros H1; rewrite H1; intros. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros | auto | auto ]. elim def_representant_unitaire2 with (A := A) (B := C) (C := C'); [ intros | auto | auto ]. elim H8; intros H9 H10; try clear H8; try exact H10. elim H6; intros H8 H11; try clear H6; try exact H11. cut (A <> B'); intros; auto with geo. cut (A <> C'); intros; auto with geo. apply oppose_representant_unitaire; auto. rewrite <- H4; rewrite <- H3. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B') (k := -1); intros D; intros. rewrite <- H13. replace D with C'; auto. cut (scalaire (vec A D) (vec A D) = 1); intros. apply unicite_representant_angle_nul with A; auto with geo. replace (vec A D) with (vec B' A). replace (cons_AV (vec B' A) (vec A C')) with (plus (cons_AV (vec B' A) (vec A B')) (cons_AV (vec A B') (vec A C'))). rewrite <- angle_plat; [ idtac | auto ]. rewrite H2; rewrite <- add_mes_compatible. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi; auto. rewrite Chasles; auto. rewrite H13; Ringvec. rewrite H13; Simplscal; auto. Qed.