proposition: Lemma angle_nul_positif_colineaire : forall A B C : PO, A <> B -> A <> C -> cons_AV (vec A B) (vec A C) = image_angle 0 -> exists k : R, k > 0 /\ vec A C = mult_PP k (vec A B).
proof: Proof. intros A B C H H0; try assumption. cut (cons_AV (vec A B) (vec A C) = cons_AV (representant_unitaire (vec A B)) (representant_unitaire (vec A C))); auto with geo. 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 | auto ]. intros H1; rewrite H1; intros. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); [ intros | auto | auto ]. 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. elim H6; intros H8 H11; try clear H6; try exact H11. cut (C' = B'); intros. 2: apply unicite_representant_angle_nul with A; auto with geo. apply egalite_representant_unitaire; auto with geo. rewrite <- H4; rewrite <- H3; rewrite <- H6; auto. Qed.