proposition: Theorem Thales_expl : forall A B C D : PO, A <> C :>PO -> B <> D :>PO -> paralleles (droite A C) (droite B D) -> vec B A = vec D C \/ (exists k : R, (exists I : PO, vec I A = mult_PP k (vec I B) /\ vec I C = mult_PP k (vec I D))).
proof: Proof. intros A B C D H11 H10 H; try assumption. elim Thales_PP with (3 := H); auto. intros k H2. elim (classic (k = -1)); intros H3. unfold vec in |- *; left. rewrite <- H3; auto. rewrite add_PP_sym; auto. rewrite H2; auto. Ringvec. right; try assumption. exists (- k). exists (barycentre (cons 1 A) (cons k B)). split; [ try assumption | idtac ]. apply add_PP_vec_reg with (a := k) (A := barycentre (cons 1 A) (cons k B)) (B := B). rewrite add_PP_sym; auto. rewrite <- mult_1_vec; auto. rewrite def_vecteur_bary; auto. Ringvec. unfold not in |- *; intros; apply H3. replace (-1) with (-1 + (1 + k)). try ring. rewrite H0; try ring. cut (barycentre (cons 1 A) (cons k B) = barycentre (cons 1 C) (cons k D)); intros. rewrite H0; try ring. apply add_PP_vec_reg with (a := k) (A := barycentre (cons 1 C) (cons k D)) (B := D). rewrite add_PP_sym; auto. rewrite <- mult_1_vec; auto. rewrite def_vecteur_bary; auto. Ringvec. unfold not in |- *; intros; apply H3. replace (-1) with (-1 + (1 + k)). try ring. rewrite H1; try ring. elim cons_inj with (a := 1 + k) (b := 1 + k) (A := barycentre (cons 1 A) (cons k B)) (B := barycentre (cons 1 C) (cons k D)); (intros; auto). repeat rewrite <- add_PP_barycentre; auto. unfold not in |- *; intros; apply H3. replace (-1) with (-1 + (1 + k)). try ring. rewrite H0; try ring. unfold not in |- *; intros; apply H3. replace (-1) with (-1 + (1 + k)). try ring. rewrite H0; try ring. unfold not in |- *; intros; apply H3. replace (-1) with (-1 + (1 + k)). try ring. rewrite H0; try ring. Qed.