proposition: Lemma varignon' : forall A B C D I J K L, (A<>C \/ B<>D) -> 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 J L). subst. unfold Parallelogram. right. unfold Parallelogram_flat. assert_congs_perm. Name X the midpoint of B and D. induction (eq_dec_points A B). treat_equalities. assert_cols. repeat split;Cong;Col; intuition. induction (eq_dec_points A D). treat_equalities. induction (eq_dec_points X K). treat_equalities. intuition. assert_cols. assert (Cong X L K L). assert (Par B L L K /\ Par B C K X /\ Par L C L X /\ Cong B X K L /\ Cong L X K L /\ Cong B L K X /\ Cong C L K X /\ Cong L K L X /\ Cong C K L X). apply (triangle_mid_par_flat_cong B L C K L X);Col;Midpoint. intro;treat_equalities. intuition. intro;treat_equalities. intuition. spliter. Cong. repeat split. show_distinct L X . intuition. assert_diffs. ColR. Col. auto. auto. left;auto. induction (eq_dec_points B D). treat_equalities. intuition. assert (Midpoint L I K). assert (Par A B L X /\ Par A D X I /\ Par B D L I /\ Cong A I X L /\ Cong B I X L /\ Cong A L X I /\ Cong D L X I /\ Cong B X L I /\ Cong D X L I). apply (triangle_mid_par_cong A B D X L I);auto. spliter. induction (eq_dec_points C D). treat_equalities. intuition. assert_diffs. induction (eq_dec_points B C). treat_equalities. assert_cols. apply cong_col_mid. auto. ColR. Cong. assert (Par B C X K /\ Par B D K L /\ Par C D X L /\ Cong B L K X /\ Cong C L K X /\ Cong B X K L /\ Cong D X K L /\ Cong C K X L /\ Cong D K X L). apply (triangle_mid_par_cong B C D K X L);auto. spliter. induction (eq_dec_points I K). treat_equalities. assert (Parallelogram A D B C) by (apply mid_plg with I;Midpoint). assert (Parallelogram A B D C) by (apply mid_plg with L;Midpoint). exfalso. apply Plg_perm in H35. apply Plg_perm in H39. spliter. apply (plg_not_comm_1 B D A C);auto. apply cong_col_mid. auto. assert (Par I L K L). apply par_trans with B D;Par. apply col_permutation_2, par_id; Par. CongR. repeat split;Col;Cong. left. intro. treat_equalities. intuition. apply (varignon_aux A B C D);auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems