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