proposition: Lemma three_medians_intersect: forall A B C I J K, ~Col A B C -> Midpoint I B C -> Midpoint J A C -> Midpoint K A B -> exists G, Col G A I /\ Col G B J /\Col G C K.
proof: Proof. Proof with assert_all. intros. assert_diffs. Name G the intersection of the medians (A I) which is a median since H0 and (B J) which is a median since H1 of the non-flat triangle A B C H. exists G; repeat split; try assumption. Name D the symmetric of C wrt G. assert_all. show_distinct' A D. permutation_intro_in_hyps. assert (Par A D J G) by (apply (triangle_mid_par A D C G J H3 H14 H1)). show_distinct' B G. assert (Par G B A D) by (perm_apply (par_col_par A D G J B)). show_distinct' B D. assert (Par B D I G) by (apply (triangle_mid_par B D C G I H104 H14 H0)). show_distinct' A G. assert (Par G A D B) by (perm_apply (par_col_par B D G I A))... show_distinct' D G. assert (~ Col G A D) by (intro; search_contradiction). assert (Parallelogram G A D B) by (apply (par_2_plg G A D B); finish). Name Z the intersection of the diagonals (G D) and (A B) of the parallelogram H17... ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon