proposition: Lemma existence_unitaire : forall A B : PO, A <> B -> exists C : PO, alignes A B C /\ scalaire (vec A C) (vec A C) = 1 /\ scalaire (vec A B) (vec A C) >= 0.
proof: Proof. intros. cut (ex (fun C : PO => vec A C = mult_PP (/ sqrt (scalaire (vec A B) (vec A B))) (vec A B))); intros. elim H0; intros C H1; try clear H0; try exact H1. cut (/ sqrt (scalaire (vec A B) (vec A B)) * / sqrt (scalaire (vec A B) (vec A B)) * scalaire (vec A B) (vec A B) = 1); intros. exists C. split; [ try assumption | idtac ]. apply colineaire_alignes with (/ sqrt (scalaire (vec A B) (vec A B))); auto. rewrite H1. split; [ try assumption | idtac ]. Simplscal. rewrite <- H0; ring. Simplscal. apply Rmult_pos; auto with *. replace (/ sqrt (scalaire (vec A B) (vec A B)) * / sqrt (scalaire (vec A B) (vec A B))) with (/ (sqrt (scalaire (vec A B) (vec A B)) * sqrt (scalaire (vec A B) (vec A B)))); auto with real. rewrite def_sqrt; auto. auto with *. auto with *. apply Rinv_mult; auto with *. apply existence_representant_mult_vecteur; auto. Qed.