proposition: Lemma caract_representant_unitaire : forall A B C : PO, A <> B -> vec A C = representant_unitaire (vec A B) -> vec A C = mult_PP (/ distance A B) (vec A B).
proof: Proof. unfold distance in |- *; intros. cut (alignes A B C /\ scalaire (vec A C) (vec A C) = 1 /\ scalaire (vec A B) (vec A C) >= 0); intros. elim H1; intros H2 H3; elim H3; intros H4 H5; try clear H3 H1; try exact H5. halignes H2 k. rewrite H1 in H4. cut (/ scalaire (vec A B) (vec A B) = k * k); intros. cut (k = sqrt (/ scalaire (vec A B) (vec A B))); intros. rewrite H1; rewrite H6. rewrite sqrt_Rinv; auto with geo real. apply inversion_sqr; auto with geo real. rewrite H1 in H5. replace k with (k * scalaire (vec A B) (vec A B) * / scalaire (vec A B) (vec A B)). replace (k * scalaire (vec A B) (vec A B)) with (scalaire (vec A B) (mult_PP k (vec A B))). apply Rmult_pos; auto with geo real. Simplscal. field; auto with geo. replace (/ scalaire (vec A B) (vec A B)) with (1 * / scalaire (vec A B) (vec A B)). rewrite <- H4. Simplscal. field; auto with geo. field; auto with geo. apply def_representant_unitaire2; auto. Qed.