proposition: Theorem Desargues : forall A B C A1 B1 C1 S : PO, C <> C1 -> B <> B1 -> C <> S -> B <> S -> C1 <> S -> B1 <> S -> A1 <> B1 -> A1 <> C1 -> B <> C -> B1 <> C1 -> triangle A A1 B -> triangle A A1 C -> alignes A A1 S -> alignes B B1 S -> alignes C C1 S -> paralleles (droite A B) (droite A1 B1) -> paralleles (droite A C) (droite A1 C1) -> paralleles (droite B C) (droite B1 C1).
proof: Proof. intros. deroule_triangle A A1 B. deroule_triangle A A1 C. elim Thales_PP with (3 := H15); intros; auto. elim Thales_PP with (3 := H14); intros; auto. apply reciproque_Thales_PP with x; auto. elim (classic (1 + x = 0)); intros. cut (x = -1); [ intros | auto ]. rewrite H27 in H24. absurd (add_PP (cons 1 A) (cons (-1) A1) = add_PP (cons 1 C) (cons (-1) C1)); auto. apply parallelogramme_non_concours with S; auto. replace x with (-1 + (1 + x)); auto. rewrite H26. ring. ring. elim (classic (1 + x0 = 0)); intros. cut (x0 = -1); [ intros | auto ]. rewrite H28 in H25. absurd (add_PP (cons 1 A) (cons (-1) A1) = add_PP (cons 1 B) (cons (-1) B1)); auto. apply parallelogramme_non_concours with S; auto. replace x0 with (-1 + (1 + x0)); auto. rewrite H27. ring. ring. rewrite add_PP_barycentre; auto. rewrite add_PP_barycentre; auto. cut (barycentre (cons 1 A) (cons x A1) = barycentre (cons 1 C) (cons x C1)); intros. cut (barycentre (cons 1 A) (cons x0 A1) = barycentre (cons 1 B) (cons x0 B1)); intros. cut (S = barycentre (cons 1 A) (cons x A1) /\ S = barycentre (cons 1 A) (cons x0 A1)); intros. cut (x = x0); [ intros | auto ]. elim H30; intros; try clear H30. rewrite <- H28; auto. rewrite H31. rewrite <- H29; auto. apply unicite_coef_bar with (A := A) (B := A1) (x := x) (x0 := x0); auto. elim H30; intros; try clear H30. rewrite <- H31; auto. split; [ try assumption | idtac ]. apply concours_unique with (A := A) (B := C) (A1 := A1) (B1 := C1); auto with geo. rewrite H28. rewrite permute_barycentre; auto. apply barycentre_alignes; auto. replace (x + 1) with (1 + x); auto. ring. apply concours_unique with (A := A) (B := B) (A1 := A1) (B1 := B1); auto with geo. rewrite H29. rewrite permute_barycentre; auto. apply barycentre_alignes; auto. replace (x0 + 1) with (1 + x0); auto. ring. apply conversion_PP with (a := 1 + x0) (b := 1 + x0); auto with *. rewrite <- add_PP_barycentre; auto. rewrite <- add_PP_barycentre; auto. apply conversion_PP with (a := 1 + x) (b := 1 + x); auto with *. rewrite <- add_PP_barycentre; auto. rewrite <- add_PP_barycentre; auto. Qed.