(* Roland Coghetto, 29 March 2018, 
                    04 April 2018.
   GNU Lesser General Public License v3.0 
   See LICENSE GeoCoq 2.3.0
     
     MOTIVATION: 
     
      - Existence of a rhombus (absolute geometry).
      - Unicity of rhomus with 3 points determinated (absolute geometry).
      
     TODO:
     
      29 march 2018 - In Euclidean geometry, construction of a rhombus from 3 determined points. DONE
                    - What about rhombus in non-euclidean geometry case ?
      04 april 2018 - MOVE all "Plg"'s lemma in quadrialterals.v 
                       (after modify context Tarski_2D by 
                          Tarski_neutral_dimensionless_with_decidable_point_equality 
                          in quadrilaterals.v) ?
                    - MOVE all "rhombus"'s lemma in quadrilaterals.v
                       (after modify context Tarski_2D by 
                          Tarski_neutral_dimensionless_with_decidable_point_equality 
                          in quadrilaterals.v) ?
                    - DELETE rhombus.v
                    - EXPERIMENTAL: (in quadrilaterals_inter_dec.v)
                        Lemma rmb_cong :
                          forall A B C D,
                          Rhombus A B C D ->
                          Cong A B B C /\ Cong A B C D /\ Cong A B D A.
                        TRY MODIFY CONTEXT ? Tarski_2D_euclidean -> Tarski_2D or Tarski_neutral_dimensionless_with_decidable_point_equality

   CHANGES: 04 april 2018, RC
   1) See JNarboux, comments about pull requests Rhombus.
   2) ADD End Rhombus_Existence_Unicity.
   2) MODIFY CONTEXT: Tarski_2D by Tarski_neutral_dimensionless_with_decidable_point_equality.
   3) ADD Existence Plg, Rhombus.

*)

Require Export GeoCoq.Tarski_dev.Annexes.perp_bisect.

Section Rhombus_Existence_Unicity.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma PlgLeft: forall A B C D, Plg A B C D -> (A <> C \/ B <> D).
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D)) *)
  unfold Plg in H. spliter.
(* Goal: @Cong Tn A B B C *)
assumption.
Qed.

Lemma PlgEquivDef: forall A B C D, (A <> C \/ B <> D) -> ((exists M,
OnCircle C M A /\ OnCircle D M B /\ Bet C M A /\ Bet D M B) <-> Plg A B C D).
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  - intros.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@OnCircle Tn C M A) (and (@OnCircle Tn D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    unfold OnCircle in *.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
    split. 
(* Goal: @Cong Tn A B B C *)
    assumption.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn M C M A) (and (@Cong Tn M D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    ex_and H0 M.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A B) (@Midpoint Tn M C1 x)) *)
(* Goal: @Rhombus Tn A C1 B x *)
    exists M.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
    split.
(* Goal: @Midpoint Tn M B D *)
    { unfold Midpoint.
(* Goal: and (@Bet Tn B M D) (@Cong Tn B M M D) *)
      split;Between. 
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
      Cong. 
    }
(* Goal: @Midpoint Tn M B D *)
    { unfold Midpoint in *.
(* Goal: and (@Bet Tn B M D) (@Cong Tn B M M D) *)
      split;Between. 
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
      Cong.
    }
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  - intros.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@OnCircle Tn C M A) (and (@OnCircle Tn D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    unfold OnCircle in *.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn M C M A) (and (@Cong Tn M D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    ex_and H0 M.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn M C M A) (and (@Cong Tn M D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    ex_and H1 M1.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn M C M A) (and (@Cong Tn M D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    unfold Midpoint in *.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Cong Tn M C M A) (and (@Cong Tn M D M B) (and (@Bet Tn C M A) (@Bet Tn D M B)))) *)
    exists M1.
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
    split;Cong.
(* Goal: and (@Cong Tn M1 D M1 B) (and (@Bet Tn C M1 A) (@Bet Tn D M1 B)) *)
    split;[Cong|Between].
Qed.

Lemma PlgAABB: forall A B, A <> B -> Plg A A B B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: @Plg Tn A C1 B x *)
(* Goal: @Rhombus Tn A C1 B x *)
  unfold Plg.
(* Goal: and (@Midpoint Tn M A B) (@Midpoint Tn M A B) *)
  split;auto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A B) (@Midpoint Tn M A B)) *)
  midpoint M A B.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A B) (@Midpoint Tn M C1 x)) *)
(* Goal: @Rhombus Tn A C1 B x *)
  exists M.
(* Goal: and (@Midpoint Tn M A B) (@Midpoint Tn M A B) *)
  split;auto.
Qed.

Lemma PlgEx: exists A B C D, Plg A B C D.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Plg Tn A B C D)))) *)
  destruct two_distinct_points as [A [B H]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Plg Tn A B C D)))) *)
  exists A, A, B, B.
(* Goal: @Plg Tn A A B B *)
  apply PlgAABB.
(* Goal: @Cong Tn A B B C *)
  assumption.
Qed.

Lemma RhombusEx: exists A B C D, Rhombus A B C D.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  destruct lower_dim_ex as [A [B [C HNC]]].
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  assert (H1 : ~ Col A B C) by auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  clear HNC.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  assert_diffs.
  assert (HAB := perp_bisect_existence A B);
  destruct HAB as [C1 [C2 HAB]]; try (assert_diffs; assumption).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  assert(Cong A C1 B C1).
(* Goal: @Cong Tn A C1 B C1 *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  apply perp_bisect_cong_2 with C2.
(* Goal: @Perp_bisect Tn C2 C1 A B *)
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  apply perp_bisect_sym_1.
(* Goal: @Cong Tn A B B C *)
  assumption.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  unfold Perp_bisect in HAB.
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  unfold ReflectL in *.
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
  destruct H0 as [M H0];
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  assert(H10 := H).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  unfold Midpoint in H10.
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  assert (exists x, Bet C1 M x /\ Cong M x C1 M) by (apply segment_construction).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D)))) *)
  ex_and H8 x.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)) *)
  exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D))) *)
  exists C1.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B B)) *)
(* Goal: @Cong Tn A B B C *)
  exists B.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A C1 B D) *)
  exists x.
(* Goal: @Rhombus Tn A C1 B x *)
  assert(Plg A C1 B x).
(* Goal: @Plg Tn A C1 B x *)
(* Goal: @Rhombus Tn A C1 B x *)
  unfold Plg.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A B) (@Midpoint Tn M C1 x)) *)
(* Goal: @Rhombus Tn A C1 B x *)
  exists M.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: @Cong Tn A B B C *)
  apply l7_2;assumption.
(* Goal: @Midpoint Tn M C1 x *)
(* Goal: @Rhombus Tn A C1 B x *)
  unfold Midpoint.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: @Cong Tn A B B C *)
  assumption.
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
  Cong.
(* Goal: @Rhombus Tn A C1 B x *)
  unfold Rhombus.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: @Cong Tn A B B C *)
  assumption.
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
  Cong.
Qed.

Lemma RhombusUnicity: forall A B C D E, Rhombus A B C D -> Rhombus A B C E -> D = E.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: @Rhombus Tn A B C D *)
  unfold Rhombus in *.
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
(* Goal: @Plg Tn A B C B *)
(* Goal: @Cong Tn A B B C *)
  unfold Plg in *.
(* Goal: @eq (@Tpoint Tn) D E *)
  spliter.
(* Goal: @eq (@Tpoint Tn) D E *)
  ex_and H4 M.
(* Goal: @eq (@Tpoint Tn) D E *)
  ex_and H3 N.
(* Goal: @eq (@Tpoint Tn) D E *)
  assert (M = N). 
(* Goal: @Cong Tn A B B C *)
  apply l7_17 with A C;assumption.
(* Goal: @eq (@Tpoint Tn) D E *)
  subst.
(* Goal: @Cong Tn A B B C *)
  apply symmetric_point_uniqueness with B N;assumption.
Qed.

Lemma ColCongMid: forall A B C, A <> C -> Col A B C -> Cong A B B C -> Midpoint B A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  assert(Col A B C). Col.
(* Goal: @Cong Tn B A B C *)
(* Goal: @Midpoint Tn B A C *)
  assert(Cong B A B C). Cong.
(* Goal: @Midpoint Tn B A C *)
  assert(A = C \/ Midpoint B A C).
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  apply l7_20; tauto. 
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  tauto.
Qed.

Lemma PlgExABC1: forall A B C, A <> C -> Col A B C -> Cong A B B C -> exists D, Plg A B C D.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Plg Tn A B C D) *)
  unfold Col in H0.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  assert(Midpoint B A C).
  apply ColCongMid;
(* Goal: @Midpoint Tn B A C *)
(* Goal: @Midpoint Tn B B B *)
  trivial.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B B)) *)
(* Goal: @Cong Tn A B B C *)
  exists B.
(* Goal: @Plg Tn A B C B *)
(* Goal: @Cong Tn A B B C *)
  unfold Plg in *.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B B)) *)
(* Goal: @Cong Tn A B B C *)
  exists B.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: @Midpoint Tn B A C *)
(* Goal: @Midpoint Tn B B B *)
  trivial.
(* Goal: @Midpoint Tn B B B *)
(* Goal: @Cong Tn A B B C *)
  Midpoint.
Qed.

Lemma PlgExABC2: forall A B C, ~Col A B C -> Cong A B B C -> exists D, Plg A B C D.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Plg Tn A B C D) *)
  intros A B C HC H.
(* Goal: @Plg Tn A B C B *)
(* Goal: @Cong Tn A B B C *)
  unfold Plg in *.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  assert(Is_on_perp_bisect B A C). exact H.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  destruct (midpoint_existence A B) as [X H1].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  destruct (l10_2_existence A C B) as [D H3].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  unfold Reflect in H3.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  unfold ReflectL in H3.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  induction (eq_dec_points A C).
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
  case H3.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
    - intros. tauto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
    - intros.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      unfold Midpoint in H4.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct (midpoint_existence A C) as [Y H5].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct (symmetric_point_construction B Y) as [E H6].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      exists E.
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      assert(B <> E).
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      induction (eq_dec_points B E).
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      subst E.
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      assert(Y = B).
(* Goal: @eq (@Tpoint Tn) Y B *)
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      apply l7_3. exact H6.
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      subst Y.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      assert(Col A B C). Col. tauto. tauto. 
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
      split. tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E)) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      exists Y.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      tauto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
    - intros.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct H3.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct H3;destruct H4;destruct H4.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct H4.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      unfold Midpoint in H4.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct (midpoint_existence A C) as [Y H7].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      destruct (symmetric_point_construction B Y) as [E H8].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      exists E.
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      assert(B <> E).
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      induction (eq_dec_points B E).
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      subst E.
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      assert(Y = B).
(* Goal: @eq (@Tpoint Tn) Y B *)
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      apply l7_3. exact H8.
(* Goal: not (@eq (@Tpoint Tn) B B) *)
(* Goal: not (@eq (@Tpoint Tn) B E) *)
(* Goal: and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B E))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      subst Y.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      assert(Col A B C). Col. tauto. tauto. 
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
      split. tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B E)) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (or (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B D))) (@ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)))) *)
      exists Y.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      tauto.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
      exists D.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
      split.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B D)) *)
      exists A.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
      tauto.
Qed.

Lemma RhombusExABC1: forall A B C, A <> C -> Col A B C -> Cong A B B C -> exists D, Rhombus A B C D.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  assert(Midpoint B A C).
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  apply ColCongMid; tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B B)) *)
(* Goal: @Cong Tn A B B C *)
  exists B.
(* Goal: @Rhombus Tn A B C D *)
  unfold Rhombus in *.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: @Plg Tn A B C B *)
(* Goal: @Cong Tn A B B C *)
  unfold Plg in *.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  tauto.
(* Goal: @ex (@Tpoint Tn) (fun M : @Tpoint Tn => and (@Midpoint Tn M A C) (@Midpoint Tn M B B)) *)
(* Goal: @Cong Tn A B B C *)
  exists B.
(* Goal: and (@Midpoint Tn B A C) (@Midpoint Tn B B B) *)
(* Goal: @Cong Tn A B B C *)
  split. 
(* Goal: @Cong Tn A B B C *)
  assumption. 
(* Goal: @Midpoint Tn B B B *)
(* Goal: @Cong Tn A B B C *)
  Midpoint. 
(* Goal: @Cong Tn A B B C *)
  assumption.
Qed.

Lemma RhombusExABC2: forall A B C, ~Col A B C -> Cong A B B C -> exists D, Rhombus A B C D.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Cong Tn A B B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  intros.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  assert(exists D, Plg A B C D).
(* Goal: @Midpoint Tn B A C *)
(* Goal: @Midpoint Tn B B B *)
  apply PlgExABC2;trivial.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  destruct H1 as [D H2].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @Rhombus Tn A B C D) *)
  exists D.
(* Goal: @Rhombus Tn A B C D *)
  unfold Rhombus in *.
(* Goal: and (@Plg Tn A B C D) (@Cong Tn A B B C) *)
  tauto.
Qed.

End Rhombus_Existence_Unicity.


