proposition: Lemma angle_produit_positif_r2 : forall (k : R) (A B C D : PO), A <> B -> C <> D -> k > 0 -> cons_AV (vec C D) (mult_PP k (vec A B)) = cons_AV (vec C D) (vec A B).
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. rewrite (angle_produit_positif_r (k:=k) (A:=A) (B:=B) (C:=E) (D:=C) (E:=D)); auto. Qed.