proposition: Lemma produit_positif_representant_unitaire : forall (k : R) (A B C : PO), A <> B :>PO -> k > 0 -> vec A C = mult_PP k (vec A B) :>PP -> representant_unitaire (vec A B) = representant_unitaire (vec A C).
proof: Proof. intros. cut (A <> C); intros. 2: apply distinct_produit_vecteur with (3 := H1); auto with real. deroule_representant_unitaire A B B'. rewrite <- H3. cut (scalaire (vec A C) (vec A B') >= 0); intros. apply def_representant_unitaire; auto. apply alignes_trans with B; auto. apply colineaire_alignes with k; auto. rewrite H1. replace (scalaire (mult_PP k (vec A B)) (vec A B')) with (k * scalaire (vec A B) (vec A B')); [ idtac | Simplscal ]. apply Rmult_pos; auto with geo. apply Rgt_ge; auto. Qed.