proposition: Lemma varignon : forall A B C D I J K L, A<>C -> B<>D -> ~ Col I J K -> Midpoint I A B -> Midpoint J B C -> Midpoint K C D -> Midpoint L A D -> Parallelogram I J K L.
proof: Proof. intros. assert_diffs. assert (Par I L B D) by perm_apply (triangle_mid_par B D A L I). assert (Par J K B D) by perm_apply (triangle_mid_par B D C K J). assert (Par I L J K) by (apply par_trans with B D;finish). assert (Par I J A C) by perm_apply (triangle_mid_par A C B J I). assert (Par L K A C) by perm_apply (triangle_mid_par A C D K L). assert (Par I J K L) by (apply par_trans with A C;finish). apply par_2_plg;finish. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems