proposition: Lemma oppose_representant_unitaire : forall A B C : PO, A <> B :>PO -> A <> C :>PO -> representant_unitaire (vec A C) = mult_PP (-1) (representant_unitaire (vec A B)) :>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 (representant_unitaire (vec A C) = representant_unitaire (vec A C')); intros. elim egalite_representant_unitaire with (A := A) (B := C) (C := C'); [ intros k H12; try clear egalite_representant_unitaire; try exact H12 | auto with geo | auto with geo | auto with geo ]. elim H12; intros H13 H14; try clear H12; try exact H14. cut (representant_unitaire (vec A B) = representant_unitaire (vec A B')); intros. elim egalite_representant_unitaire with (A := A) (B := B) (C := B'); [ intros k0 H12; try clear egalite_representant_unitaire; try exact H12 | auto with geo | auto with geo | auto with geo ]. elim H12; intros H15 H16; try clear H12; try exact H16. cut (k <> 0); auto with real; intros. replace (vec A C) with (mult_PP (/ k) (vec A C')); idtac. rewrite H1; rewrite H16. exists (- (/ k * k0)). split; [ idtac | Ringvec ]. cut (/ k * k0 > 0); intros; auto with real. apply Rmult_gt_0_compat; auto with *. rewrite H14. Fieldvec k. rewrite H3; (symmetry in |- *; auto with geo). rewrite H4; (symmetry in |- *; auto with geo). Qed.