proposition: Lemma unicite_representant_unitaire : forall A B C D : PO, A <> B -> alignes A B C -> scalaire (vec A C) (vec A C) = 1 -> scalaire (vec A B) (vec A C) >= 0 -> alignes A B D -> scalaire (vec A D) (vec A D) = 1 -> scalaire (vec A B) (vec A D) >= 0 -> C = D.
proof: Proof. intros. halignes H0 k. halignes H3 k0. cut (k = k0); intros. apply conversion_PP with (a := 1) (b := 1); auto with *. RingPP2 H6. RingPP2 H7. rewrite H8; RingPP. apply resolution; auto. replace k with (k * scalaire (vec A B) (vec A C) * / scalaire (vec A B) (vec A C)). replace (k * scalaire (vec A B) (vec A C)) with (scalaire (mult_PP k (vec A B)) (vec A C)). rewrite <- H6; rewrite H1. replace (1 * / scalaire (vec A B) (vec A C)) with (/ scalaire (vec A B) (vec A C)); try ring. apply Rinv_le_pos; auto with geo real. Simplscal. field. auto with geo. replace k0 with (k0 * scalaire (vec A B) (vec A D) * / scalaire (vec A B) (vec A D)). replace (k0 * scalaire (vec A B) (vec A D)) with (scalaire (mult_PP k0 (vec A B)) (vec A D)). rewrite <- H7; rewrite H4. replace (1 * / scalaire (vec A B) (vec A D)) with (/ scalaire (vec A B) (vec A D)); try ring. apply Rinv_le_pos; auto with geo real. Simplscal. field. auto with geo. cut (scalaire (vec A C) (vec A C) = scalaire (vec A D) (vec A D)); intros. rewrite H7 in H8; rewrite H6 in H8. replace (k * k) with (scalaire (mult_PP k (vec A B)) (mult_PP k (vec A B)) * / scalaire (vec A B) (vec A B)). replace (k0 * k0) with (scalaire (mult_PP k0 (vec A B)) (mult_PP k0 (vec A B)) * / scalaire (vec A B) (vec A B)). rewrite H8; auto. field_simplify_eq. Simplscal. auto with geo. field_simplify_eq. Simplscal. auto with geo. rewrite H4; auto. Qed.