Require Export GeoCoq.Tarski_dev.Annexes.midpoint_theorems.

Section Varignon.

Context `{TE:Tarski_euclidean}.

(** This is the usual proof presented in classroom based on
the midpoint theorem but this proof suffers from two problems.
It needs the fact that IJK are not collinear, 
which is not always the case when the quadrilateral is not convex. 
It also needs the fact that A is different from C, and B is different from D.
The original proof by Varignon suffer from the same problem.
The original proof can be found page 138, Corollary IV:
http://polib.univ-lille3.fr/documents/B590092101_000000011.489_IMT.pdf
*)

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.
(* Goal: forall (A B C D I J K L : @Tpoint Tn) (_ : or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (_ : @Midpoint Tn I A B) (_ : @Midpoint Tn J B C) (_ : @Midpoint Tn K C D) (_ : @Midpoint Tn L A D), @Parallelogram Tn I J K L *)
intros.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
assert_diffs.
assert (Par I L B D) (** Applying the midpoint theorem in the triangle BDA. *)
  by perm_apply (triangle_mid_par B D A L I).
assert (Par J K B D) (** Applying the midpoint theorem in the triangle BDC. *)
  by perm_apply (triangle_mid_par B D C K J).
assert (Par I L J K) (** Transitivity of parallelism *)
  by (apply par_trans with B D;finish).
assert (Par I J A C) (** Applying the midpoint theorem in the triangle ACB. *)
  by perm_apply (triangle_mid_par A C B J I). 
assert (Par L K A C) (** Applying the midpoint theorem in the triangle ACD. *)
  by perm_apply (triangle_mid_par A C D K L).
assert (Par I J K L) (** Transitivity of parallelism *)
  by (apply par_trans with A C;finish).
(* Goal: @Parallelogram Tn I J K L *)
apply par_2_plg;finish. (** If in the opposite side of quadrilatral are parallel and two opposite side are distinct
                            then it is a parallelogram. *)
Qed.

(** We propose here a more complex proof to simplify the ndg. 
If we know that a quadrilateral has its pairs of opposite side congruent and parallel
 then it is a parallelogram. *)


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.
(* Goal: forall (A B C D I J K L : @Tpoint Tn) (_ : or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (_ : @Midpoint Tn I A B) (_ : @Midpoint Tn J B C) (_ : @Midpoint Tn K C D) (_ : @Midpoint Tn L A D), @Parallelogram Tn I J K L *)
intros.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points B D).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
treat_equalities.
(* Goal: @Parallelogram Tn L K K L *)
(* Goal: @Parallelogram Tn I J K L *)
apply plg_trivial.
(* Goal: not (@eq (@Tpoint Tn) J L) *)
(* Goal: @Parallelogram Tn I J K L *)
intro;treat_equalities;intuition.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
Name X the midpoint of B and D.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).

(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: @Parallelogram Tn I J K L *)
apply par_par_cong_cong_parallelogram;finish.
Qed.


Lemma varignon_aux :
 forall A B C D I J K L,
  (A<>C \/ B<>D) ->
  J<>L ->
  Midpoint I A B ->
  Midpoint J B C ->
  Midpoint K C D ->
  Midpoint L A D ->
  Parallelogram I J K L.
Proof.
(* Goal: forall (A B C D I J K L : @Tpoint Tn) (_ : or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (_ : @Midpoint Tn I A B) (_ : @Midpoint Tn J B C) (_ : @Midpoint Tn K C D) (_ : @Midpoint Tn L A D), @Parallelogram Tn I J K L *)
intros.
(* Goal: @Parallelogram Tn I J K L *)
induction H.
(* Goal: @Parallelogram Tn I J K L *)
(* Goal: @Parallelogram Tn I J K L *)
eauto using varignon_aux_aux.

(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points A C).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
treat_equalities.
(* Goal: @Parallelogram Tn J J L L *)
(* Goal: @Parallelogram Tn I J K L *)
apply plg_trivial1.
(* Goal: not (@eq (@Tpoint Tn) J L) *)
(* Goal: @Parallelogram Tn I J K L *)
intro;treat_equalities;intuition.

(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
Name X the midpoint of B and D.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).

(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: @Parallelogram Tn I J K L *)
apply par_par_cong_cong_parallelogram;finish.
Qed.

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.
(* Goal: forall (A B C D I J K L : @Tpoint Tn) (_ : or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (_ : @Midpoint Tn I A B) (_ : @Midpoint Tn J B C) (_ : @Midpoint Tn K C D) (_ : @Midpoint Tn L A D), @Parallelogram Tn I J K L *)
intros.
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points J L).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
subst.
(* Goal: @Parallelogram Tn I L K L *)
(* Goal: @Parallelogram Tn I J K L *)
unfold Parallelogram.
(* Goal: or (@Parallelogram_strict Tn I L K L) (@Parallelogram_flat Tn I L K L) *)
(* Goal: @Parallelogram Tn I J K L *)
right.
(* Goal: @Parallelogram_flat Tn I L K L *)
(* Goal: @Parallelogram Tn I J K L *)
unfold Parallelogram_flat.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
assert_congs_perm.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
Name X the midpoint of B and D.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points A B).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 treat_equalities.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 assert_cols.
(* Goal: and (@Col Tn I X K) (and (@Col Tn I X X) (and (@Cong Tn I X K X) (and (@Cong Tn I X K X) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) X X)))))) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 repeat split;Cong;Col; intuition.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points A D).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 treat_equalities.
(* Goal: and (@Col Tn X L K) (and (@Col Tn X L L) (and (@Cong Tn X L K L) (and (@Cong Tn X L K L) (or (not (@eq (@Tpoint Tn) X K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 induction (eq_dec_points X K).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
  treat_equalities.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
  intuition.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 assert_cols.
(* Goal: and (@Col Tn X L K) (and (@Col Tn X L L) (and (@Cong Tn X L K L) (and (@Cong Tn X L K L) (or (not (@eq (@Tpoint Tn) X K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 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).
(* Goal: and (@Par Tn B L L K) (and (@Par Tn B C K X) (and (@Par Tn L C L X) (and (@Cong Tn B X K L) (and (@Cong Tn L X K L) (and (@Cong Tn B L K X) (and (@Cong Tn C L K X) (and (@Cong Tn L K L X) (@Cong Tn C K L X)))))))) *)
(* Goal: @Cong Tn X L K L *)
(* Goal: and (@Col Tn X L K) (and (@Col Tn X L L) (and (@Cong Tn X L K L) (and (@Cong Tn X L K L) (or (not (@eq (@Tpoint Tn) X K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  apply (triangle_mid_par_flat_cong B L C K L X);Col;Midpoint.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
   intro;treat_equalities. intuition.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
   intro;treat_equalities. intuition.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
   spliter.
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
   Cong.
(* Goal: and (@Col Tn X L K) (and (@Col Tn X L L) (and (@Cong Tn X L K L) (and (@Cong Tn X L K L) (or (not (@eq (@Tpoint Tn) X K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 repeat split.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 show_distinct L X . intuition.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 assert_diffs.
(* Goal: @Col Tn I L X *)
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 ColR.
(* Goal: @Col Tn X L L *)
(* Goal: @Cong Tn X L K L *)
(* Goal: @Cong Tn X L K L *)
(* Goal: or (not (@eq (@Tpoint Tn) X K)) (not (@eq (@Tpoint Tn) L L)) *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 Col.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 auto.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 auto.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 left;auto.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points B D).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 treat_equalities. intuition.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
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).
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
apply (triangle_mid_par_cong A B D X L I);auto.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
spliter.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points C D).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 treat_equalities.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 intuition.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
assert_diffs.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points B C).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
 treat_equalities.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 assert_cols.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 apply cong_col_mid.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  auto.
(* Goal: @Col Tn I L X *)
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  ColR.
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 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).
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
apply (triangle_mid_par_cong B C D K X L);auto.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
spliter.
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
induction (eq_dec_points I K).
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
  treat_equalities.
(* Goal: @Midpoint Tn L I I *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  assert (Parallelogram A D B C) by (apply mid_plg with I;Midpoint).
(* Goal: @Midpoint Tn L I I *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  assert (Parallelogram A B D C) by (apply mid_plg with L;Midpoint).
(* Goal: @Midpoint Tn L I I *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  exfalso.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  apply Plg_perm in H39.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  apply Plg_perm in H40.
(* Goal: False *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  spliter.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  apply (plg_not_comm_1 B D A C);auto.

(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
apply cong_col_mid.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 auto.
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 assert (Par I L K L).
(* Goal: @Par Tn I L K L *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
  apply par_trans with B D;Par.
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 apply par_id_5;Par.
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
 eCong.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
assert_congs_perm.
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
assert_cols.
(* Goal: @Cong Tn I L L X *)
(* Goal: @Midpoint Tn L I K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
repeat split;Col;Cong.
(* Goal: or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)) *)
(* Goal: @Parallelogram Tn I J K L *)
left.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Parallelogram Tn I J K L *)
intro.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
subst.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
treat_equalities.
(* Goal: False *)
(* Goal: @Parallelogram Tn I J K L *)
intuition.
(* Goal: not (@eq (@Tpoint Tn) I K) *)
(* Goal: @Col Tn I L K *)
(* Goal: @Cong Tn I L L K *)
(* Goal: and (@Col Tn I L K) (and (@Col Tn I L L) (and (@Cong Tn I L K L) (and (@Cong Tn I L K L) (or (not (@eq (@Tpoint Tn) I K)) (not (@eq (@Tpoint Tn) L L)))))) *)
(* Goal: @Parallelogram Tn I J K L *)
eapply varignon_aux;eauto.
Qed.



End Varignon.
