proposition: Lemma couple_colineaires_parallelogramme : forall (A B C D : PO) (k k' : R), A <> B -> ~ alignes A B C -> vec C D = mult_PP k (vec A B) -> vec B D = mult_PP k' (vec A C) -> vec B D = vec A C.
proof: Proof. unfold vec in |- *; intros. cut (cons 1 D = add_PP (add_PP (cons (- k') A) (cons 1 B)) (cons (1 + - (- k' + 1)) C)); intros. cut (cons 1 D = add_PP (add_PP (cons (- k) A) (cons k B)) (cons (1 + - (- k + k)) C)); intros. cut (k = k' /\ k = 1); intros. elim H5; intros H6 H7; try clear H5; try exact H7. rewrite <- H6 in H2; rewrite H7 in H2. rewrite H2; Ringvec. cut (- k = - k' /\ k = 1); intros. elim H5; intros H6 H7; try clear H5; try exact H7. split; [ idtac | try assumption ]. replace k with (- - k). rewrite H6; ring. ring. apply (unicite_coor_bar2 (A:=A) (B:=B) (C:=C) (I:=D)); auto. RingPP2 H1. RingPP. RingPP2 H2. RingPP. Qed.