proposition: Lemma angle_produit_positif_l : forall (k : R) (A B C D : PO), A <> B -> C <> D -> k > 0 -> cons_AV (mult_PP k (vec A B)) (vec C D) = cons_AV (vec A B) (vec C D).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); intros E H2; try clear existence_representant_mult_vecteur; rewrite <- H2. cut (A <> E); intros. cut (cons_AV (vec C D) (vec A E) = cons_AV (vec C D) (vec A B)); intros. 2: rewrite (angle_produit_positif_r (k:=k) (A:=A) (B:=B) (C:=E) (D:=C) (E:=D)) ; auto. apply permute_angles; auto. apply distinct_produit_vecteur with (3 := H2); auto with real. Qed.