proposition: Lemma quadrileral_midpoints: forall A B C D I J K L X Y, ~ Col I J K -> Midpoint I A B -> Midpoint J B C -> Midpoint K C D -> Midpoint L A D -> Midpoint X I K -> Midpoint Y J L -> X = Y.
proof: Proof. intros. assert_diffs_by_cases. assert (Parallelogram I J K L) by (apply (varignon A B C D I J K L);finish). assert (Midpoint X J L) by (perm_apply (plg_mid_2 I J K L X)). treat_equalities;trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon