proposition: Lemma varignon_aux_aux : forall A B C D I J K L, A<>C -> J<>L -> Midpoint I A B -> Midpoint J B C -> Midpoint K C D -> Midpoint L A D -> Parallelogram I J K L.
proof: Proof. intros. induction (eq_dec_points B D). treat_equalities. apply plg_trivial. intro;treat_equalities;intuition. Name X the midpoint of B and D. assert_diffs. assert (Par B D L I /\ Cong B X L I) by (apply (triangle_mid_par_cong_1 A B D X L I);finish). assert (Par B D K J /\ Cong B X K J) by (apply (triangle_mid_par_cong_1 C B D X K J);finish). spliter. assert (Par I L J K) by (eapply par_trans with B D;finish). assert (Cong I L J K) by (eapply cong_transitivity with B X;finish). Name X' the midpoint of A and C. assert (Par A C J I /\ Cong A X' J I) by (apply (triangle_mid_par_cong_1 B A C X' J I);finish). assert (Par A C K L /\ Cong A X' K L) by (apply (triangle_mid_par_cong_1 D A C X' K L);finish). spliter. assert (Par I J K L) by (eapply par_trans with A C;finish). assert (Cong I J K L) by (eapply cong_transitivity with A X';finish). apply par_par_cong_cong_parallelogram;finish. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems