proposition: Lemma alignes_distance_negatif_colineaire : forall (k : R) (A B C : PO), A <> B -> A <> C -> cons_AV (vec A B) (vec A C) = image_angle pi -> distance A C = k * distance A B -> vec A C = mult_PP (- k) (vec A B).
proof: Proof. intros. elim angle_pi_negatif_colineaire with (A := A) (B := B) (C := C); [ intros k0 H3; elim H3; intros H4 H5; try clear H3; try exact H5 | auto | auto | auto ]. replace k with (- k0). replace (- - k0) with k0; try ring; auto. cut (distance A C = - k0 * distance A B); intros; auto. apply Rmult_eq_reg_l with (distance A B); auto with geo. replace (distance A B * -k0) with (distance A C) by (rewrite H3 in |- *; ring). rewrite H2 in |- *; ring. replace (- k0) with (Rabs k0); auto with geo. apply Rabs_left; auto with real. Qed.