proposition: Lemma produit_negatif_representant_unitaire : forall (k : R) (A B C : PO), A <> B -> k < 0 -> vec A C = mult_PP k (vec A B) -> representant_unitaire (vec A C) = mult_PP (-1) (representant_unitaire (vec A B)).
proof: Proof. intros. cut (A <> C); intros. 2: apply distinct_produit_vecteur with (3 := H1); auto. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H3; try clear existence_representant_unitaire; try exact H3 | auto ]. rewrite <- H3. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros; elim H5; intros H6 H7; try clear H5; try exact H6 | auto | auto ]. cut (- scalaire (vec A C) (vec A B') >= 0); intros. symmetry in |- *. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B') (k := -1); intros D H9; try clear existence_representant_mult_vecteur; rewrite <- H9. apply def_representant_unitaire; auto. apply alignes_trans with B; auto. apply colineaire_alignes with k; auto. halignes H4 k0. apply colineaire_alignes with (- k0); auto. rewrite H9; rewrite H8; Ringvec. rewrite H9; Simplscal; auto. rewrite H9; Simplscal; auto. rewrite H1; Simplscal. apply Rmult_pos; auto. apply Rgt_ge; auto with real. auto with real. Qed.