proposition: Lemma Thales_concours : forall (k : R) (A B C I J : PO), triangle A B C -> k <> 0 :>R -> vec A I = mult_PP k (vec A B) :>PP -> paralleles (droite B C) (droite I J) -> alignes A C J -> vec A J = mult_PP k (vec A C) :>PP.
proof: Proof. intros k A B C I J H H0 H2 H3 H4; try assumption. elim (classic (k = 1)); intros. cut (B = I); intros. cut (J = C); intros. rewrite H6; rewrite H1; Ringvec. generalize (alignes_paralleles_confondus (A:=A) (B:=B)); intros H16; apply H16; auto. pattern B at 2 in |- *; rewrite H5; auto. apply vecteur_nul_conf. replace (vec B I) with (add_PP (mult_PP (-1) (vec A B)) (vec A I)); [ idtac | Ringvec ]. rewrite H2; rewrite H1; Ringvec. generalize H2; unfold vec in |- *; intros H98. deroule_triangle A B C. cut (1 + - k <> 0). intros H102. cut (- k <> 0). intros H103. cut (1 + - / k <> 0). intros H104. cut (B <> I). intros H99. cut (I <> J); intros. cut (alignes B I A). intros H100. cut (~ alignes B I C). intros H101. elim Thales_PP with (A := B) (B := I) (C := C) (D := J); [ intros x H10; try clear Thales_PP; try exact H10 | auto | auto | auto ]. elim (classic (x = -1)); intros. cut (C <> J); intros. rewrite H11 in H10. absurd (add_PP (cons 1 B) (cons (-1) I) = add_PP (cons 1 C) (cons (-1) J)); auto. apply parallelogramme_non_concours with A; auto with geo. red in |- *; intros; apply H99. apply conversion_PP with (a := 1) (b := 1); try ring. RingPP1 H10. rewrite H11; rewrite H12; RingPP. discrR. cut (1 + x <> 0); intros. cut (C <> J); intros. cut (barycentre (cons 1 B) (cons x I) = barycentre (cons 1 C) (cons x J)); intros. cut (cons 1 J = add_PP (cons (1 + - k) A) (cons k C)); intros. rewrite H15; RingPP. cut (A = barycentre (cons 1 B) (cons x I)); intros. cut (A = barycentre (cons (- k) B) (cons 1 I)); intros. cut (x = - / k); intros. rewrite <- H15 in H14. rewrite H17 in H14. rewrite H17 in H15. cut (A = barycentre (cons (- k) C) (cons 1 J)); intros. rewrite H18. replace (1 + - k) with (- k + 1); [ idtac | ring ]. rewrite <- add_PP_barycentre; auto. RingPP. replace (- k + 1) with (1 + - k); [ auto | ring ]. rewrite H14. rewrite <- homogene_barycentre with (k := - k); auto. replace (- k * 1) with (- k) by ring. replace (- k * - / k) with 1 by (field;trivial). reflexivity. cut (A = barycentre (cons 1 B) (cons (- / k) I)); intros. apply unicite_coef_bar with (A := B) (B := I) (x := x) (x0 := - / k); auto. rewrite <- H15; auto. rewrite H16. symmetry in |- *. rewrite <- homogene_barycentre with (k := - k); auto. replace (- k * 1) with (- k) by ring. replace (- k * - / k) with 1 by (field;trivial). reflexivity. cut (cons (1 + - k) A = add_PP (cons 1 I) (cons (- k) B)); intros. rewrite permute_barycentre; auto. apply conversion_PP with (a := 1 + - k) (b := 1 + - k); auto. rewrite <- add_PP_barycentre; auto. replace (- k + 1) with (1 + - k); [ auto | ring ]. RingPP2 H98; RingPP. apply concours_unique with (A := B) (B := C) (A1 := I) (B1 := J); auto. apply permute_alignes; auto with geo. apply barycentre_alignes; auto. rewrite H14. apply permute_alignes; auto. apply barycentre_alignes; auto. apply conversion_PP with (a := 1 + x) (b := 1 + x); auto. rewrite <- add_PP_barycentre; auto. rewrite <- add_PP_barycentre; auto. red in |- *; intros; apply H101. replace C with (barycentre (cons 1 B) (cons x I)). apply barycentre_alignes; auto. apply conversion_PP with (a := 1 + x) (b := 1 + x); try ring; auto. rewrite <- add_PP_barycentre; auto. rewrite H10; rewrite H13; Ringvec. red in |- *; intros; apply H11. replace (-1) with (-1 + 0) by ring. rewrite <- H12; ring. cut (~ alignes B A C); intros; auto with geo. red in |- *; intros; apply H10. halignes H11 y. apply colineaire_alignes with ((1 + - k) * y). rewrite H12; unfold vec in |- *. RingPP2 H98. replace (add_PP (mult_PP k (add_PP (cons (-1) A) (cons 1 B))) (mult_PP (-1) (cons (-1) A))) with (add_PP (cons (1 + - k) A) (cons k B)); [ idtac | RingPP ]. replace (add_PP (cons (-1) B) (add_PP (cons (1 + - k) A) (cons k B))) with (add_PP (cons (1 + - k) A) (cons (-1 * (1 + - k)) B)); [ idtac | RingPP ]. replace ((1 + - k) * y) with (y * (1 + - k)); [ idtac | ring ]. RingPP. apply colineaire_alignes with (/ (1 + - k)). replace (vec B I) with (add_PP (vec B A) (vec A I)); [ idtac | Ringvec ]. rewrite H2. Fieldvec (1 + - k). cut (~ alignes A C B); intros; auto with geo. red in |- *; intros; apply H9. halignes H4 x. apply colineaire_alignes with (/ k * x). apply mult_PP_regulier with k; auto. rewrite <- H2; rewrite H10; rewrite H11. Fieldvec k. red in |- *; intros; apply H102. elim produit_vecteur_nul with (a := 1 + - k) (A := A) (B := B); [ intros H10; try clear produit_vecteur_nul; try exact H10 | intros H10; try clear produit_vecteur_nul | try clear produit_vecteur_nul ]. absurd (A = B); auto. replace (mult_PP (1 + - k) (vec A B)) with (add_PP (vec A B) (mult_PP (-1) (mult_PP k (vec A B)))); [ idtac | Ringvec ]. rewrite <- H2; rewrite H9; Ringvec. replace (1 + - / k) with (- / k * (1 + - k)); try ring; auto. apply integre_not; auto with real. field. auto with real. auto with real. red in |- *; intros; apply H1. replace 1 with (1 + - k + k); [ idtac | ring ]. rewrite H9; ring. Qed.