proposition: Lemma angle_produit_negatif_r : forall (k : R) (A B C D E : PO), A <> B -> D <> E -> k < 0 -> vec A C = mult_PP k (vec A B) -> cons_AV (vec D E) (vec A C) = plus (cons_AV (vec D E) (vec A B)) (image_angle pi).
proof: Proof. intros. cut (A <> C); intros. 2: apply distinct_produit_vecteur with (3 := H2); auto. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. rewrite (produit_negatif_representant_unitaire (k:=k) (A:=A) (B:=B) (C:=C)); auto. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H4 | auto ]. rewrite <- H4. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros; elim H6; intros H7 H8; try clear H6; try exact H7 | auto | auto ]. cut (A <> B'); intros; auto with geo. replace (mult_PP (-1) (vec A B')) with (vec B' A); [ idtac | Ringvec ]. rewrite (angle_plat (A:=A) (B:=B')); auto. elim existence_representant_unitaire with (A := D) (B := E); [ intros F H9 | auto ]. elim def_representant_unitaire2 with (A := D) (B := E) (C := F); [ intros; elim H11; intros H12 H13; try clear H11; try exact H12 | auto | auto ]. cut (D <> F); intros; auto with geo. rewrite <- H9; rewrite Chasles; auto. auto with real. Qed.