proposition: Lemma egalite_representant_unitaire : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> representant_unitaire (vec A B) = representant_unitaire (vec A C) :>PP -> exists k : R, k > 0 /\ vec A C = mult_PP k (vec A B) :>PP.
proof: Proof. intros A B C H H0; try assumption. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H3; try clear existence_representant_unitaire; rewrite <- H3 | auto ]. elim existence_representant_unitaire with (A := A) (B := C); [ intros C' H4; rewrite <- H4; intros | auto ]. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros | auto | auto ]. elim H5; intros H6 H7; try clear H5; try exact H7. elim def_representant_unitaire2 with (A := A) (B := C) (C := C'); [ intros | auto | auto ]. elim H8; intros H9 H10; try clear H8; try exact H10. cut (alignes A C' C); intros; auto with geo. assert (A <> C'); auto with geo. halignes H8 k. halignes H2 k0. exists (k * k0). split; [ idtac | try assumption ]. apply Rmult_gt_0_compat. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H14 | intros H14; elim H14; [ intros H15; try clear H14; try exact H15 | intros H15; try exact H15 ] ]. absurd (scalaire (vec A C) (vec A C') >= 0); auto. rewrite H12. replace (scalaire (mult_PP k (vec A C')) (vec A C')) with (k * scalaire (vec A C') (vec A C')); [ idtac | Simplscal ]. rewrite H9. replace (k * 1) with k; [ auto with real | ring ]. absurd (A = C); auto. apply vecteur_nul_conf. rewrite H12; rewrite H15; Ringvec. elim Rtotal_order with (r1 := k0) (r2 := 0); [ intros H16; try clear total_order | intros H16; elim H16; [ intros H17; try clear H16; try exact H17 | intros H17; try exact H17 ] ]. absurd (scalaire (vec A B) (vec A B') >= 0); auto. replace (vec A B) with (mult_PP (/ k0) (vec A B')); [ Simplscal | idtac ]. rewrite H6. replace (/ k0 * 1) with (/ k0); [ idtac | ring ]. cut (/ k0 < 0); intros; auto with real. rewrite H13. cut (k0 <> 0); intros; auto with real. Fieldvec k0. absurd (scalaire (vec A B') (vec A B') = 1); auto. rewrite H13; rewrite H17; Simplscal. replace (0 * 0 * scalaire (vec A B) (vec A B)) with 0; [ auto with real | ring ]. rewrite H12; rewrite <- H1; rewrite H13; Ringvec. Qed.