 (* Gabriel Braun April 2013 *)
Require Export GeoCoq.Tarski_dev.Ch13_1.

Section Length_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** Pappus Desargues *)

(******************** length *********************)

Lemma lg_exists : forall A B, exists l, Q_Cong l /\ l A B.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: and (@Q_Cong Tn (fun C D : @Tpoint Tn => @Cong Tn A B C D)) (@Cong Tn A B A B) *)
    unfold Q_Cong.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun l : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B X Y) (l X Y)))) (l A B)) *)
    exists (fun x y => Cong A B x y).
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
      exists B.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
      intros.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
      split; auto.
(* Goal: @Cong Tn A B A B *)
    Cong.
Qed.


Lemma lg_cong : forall l A B C D, Q_Cong l -> l A B -> l C D -> Cong A B C D.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
(* Goal: l A A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    ex_and H2 Y.
(* Goal: l C D *)
    assert(HH:= H A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: @Cong Tn A B C D *)
    assert(HH:= H C D).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: @Cong Tn A B C D *)
    apply H3 in H0.
(* Goal: @Cong Tn A B C D *)
    apply H5 in H1.
(* Goal: @Cong Tn A B A B *)
    apply cong_transitivity with X Y; Cong.
Qed.

Lemma lg_cong_lg : forall l A B C D, Q_Cong l -> l A B -> Cong A B C D -> l C D.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
    ex_and H A0.
    ex_and H2 B0.
    assert(HP:= H A B).
    assert(HQ:= H C D).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HP.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HQ.
(* Goal: l C D *)
    apply H4.
    eapply cong_transitivity.
(* Goal: l X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      apply H3.
      assumption.
    assumption.
Qed.

Lemma lg_sym : forall l A B, Q_Cong l -> l A B -> l B A.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @Cong Tn A B A B *)
    apply (lg_cong_lg l A B); Cong.
Qed.

Lemma ex_points_lg : forall l, Q_Cong l -> exists A, exists B, l A B.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H A.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H0 B.
(* Goal: l C D *)
    assert(HH:= H A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
    exists B.
(* Goal: iff (l1 X Y) (l2 X Y) *)
    apply H0.
(* Goal: @Cong Tn A B A B *)
    Cong.
Qed.

End Length_1.

Ltac lg_instance l A B :=
  assert(tempo_sg:= ex_points_lg l);
  match goal with
    |H: Q_Cong l |-  _ => assert(tempo_H:=H); apply tempo_sg in tempo_H; elim tempo_H; intros A ; let tempoHP := fresh "tempo_HP" in intro tempoHP; clear tempo_H; elim tempoHP; intro B; intro; clear tempoHP
  end;
  clear tempo_sg.

Section Length_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma is_len_cong : forall A B C D l, Len A B l -> Len C D l -> Cong A B C D.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: False *)
    unfold Len in *.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: @Cong Tn A B C D *)
    eapply (lg_cong l); auto.
Qed.

Lemma is_len_cong_is_len : forall A B C D l, Len A B l -> Cong A B C D -> Len C D l.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: False *)
    unfold Len in *.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
(* Goal: l C D *)
    ex_and H a.
(* Goal: l C D *)
    ex_and H2 b.
(* Goal: l C D *)
    assert(HH:= H A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: l C D *)
    assert(HH1:= H C D).
(* Goal: l C D *)
    destruct HH1.
(* Goal: l C D *)
    apply H3 in H1.
(* Goal: l C D *)
    apply H4.
(* Goal: @Cong Tn A2 B2 A0 B0 *)
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    apply cong_transitivity with A B; trivial.
Qed.

Lemma not_cong_is_len : forall A B C D l , ~(Cong A B C D) -> Len A B l -> ~(l C D).
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: not (l C D) *)
    unfold Len in H0.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    intro.
(* Goal: @Len Tn A A la *)
(* Goal: @Len Tn A A lb *)
    apply H.
(* Goal: l1 A0 B0 *)
    apply (lg_cong l); auto.
Qed.

Lemma not_cong_is_len1 : forall A B C D l , ~Cong A B C D -> Len A B l -> ~ Len C D l.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    intro.
(* Goal: False *)
    unfold Len in *.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: @Len Tn A A la *)
(* Goal: @Len Tn A A lb *)
    apply H.
(* Goal: l1 A0 B0 *)
    apply (lg_cong l); auto.
Qed.

Lemma lg_null_instance : forall l A, Q_Cong_Null l -> l A A.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: l A A *)
    unfold Q_Cong_Null in H.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
(* Goal: l A A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
    ex_and H1 Y.
(* Goal: l A A *)
    assert(HH:= H A A).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: l A A *)
    ex_and H0 P.
(* Goal: l A A *)
    assert(HH:=(H P P)).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HH.
(* Goal: l A A *)
    apply H4 in H3.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    apply H1.
    apply cong_symmetry in  H3.
(* Goal: @Cong Tn X Y A A *)
    apply cong_reverse_identity in H3.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    subst Y.
(* Goal: @Cong Tn X X A A *)
    apply cong_trivial_identity.
Qed.

Lemma lg_null_trivial : forall l A, Q_Cong l -> l A A -> Q_Cong_Null l.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @Q_Cong_Null Tn l *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    unfold Q_Cong_Null.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
    exists A.
(* Goal: l1 A0 B0 *)
    auto.
Qed.

Lemma lg_null_dec : forall l, Q_Cong l -> Q_Cong_Null l \/ ~ Q_Cong_Null l.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @EqL Tn l1 l2 *)
    assert(HH:=H).
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    unfold Q_Cong in H.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H A.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H0 B.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    induction(eq_dec_points A B).
(* Goal: False *)
(* Goal: @Col Tn P A Q *)
      subst B.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
      left.
(* Goal: @Q_Cong_Null Tn l *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      unfold Q_Cong_Null.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
      split.
(* Goal: l1 A0 B0 *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
      exists A.
(* Goal: @Len Tn A A la *)
(* Goal: @Len Tn A A lb *)
      apply H.
(* Goal: @Cong Tn A B A B *)
      Cong.
(* Goal: or (@Q_Cong_Null Tn l) (not (@Q_Cong_Null Tn l)) *)
    right.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    intro.
(* Goal: False *)
    unfold Q_Cong_Null in H1.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: False *)
    ex_and H2 P.
(* Goal: iff (l1 X Y) (l2 X Y) *)
    apply H0.
(* Goal: @eq (@Tpoint Tn) A B *)
    assert(Cong A B P P).
(* Goal: l1 A0 B0 *)
      apply H; auto.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply cong_identity in H2.
(* Goal: l1 A0 B0 *)
    auto.
Qed.

Lemma ex_point_lg : forall l A, Q_Cong l -> exists B, l A B.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
    induction(lg_null_dec l).
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
      exists A.
(* Goal: l A A *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      apply lg_null_instance.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: @EqL Tn l1 l2 *)
      assert(HH:= H).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
      unfold Q_Cong in HH.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
      ex_and HH X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      ex_and H1 Y.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      assert(HH:= another_point A).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      ex_and HH P.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      assert(HP:= H2 X Y).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
      destruct HP.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
      assert(l X Y).
(* Goal: l X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
        apply H3.
(* Goal: @Cong Tn X Y X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
        apply cong_reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      assert(X <> Y).
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
        intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
        subst Y.
(* Goal: iff (l1 X Y) (l2 X Y) *)
        apply H0.
(* Goal: @Q_Cong_Null Tn l *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
        unfold Q_Cong_Null.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
        split.
(* Goal: l1 A0 B0 *)
          auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => l A A) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
        exists X.
(* Goal: l1 A0 B0 *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => l A B) *)
(* Goal: @Q_Cong Tn l *)
      assert(HH:= segment_construction_3 A P X Y H1 H6).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      ex_and HH B.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
      exists B.
(* Goal: l A B *)
(* Goal: @Q_Cong Tn l *)
      assert(HH:= H2 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
      destruct HH.
(* Goal: l A B *)
(* Goal: @Out Tn A B P *)
      apply H9.
(* Goal: @Cong Tn A B A B *)
      Cong.
(* Goal: l1 A0 B0 *)
    auto.
Qed.




Lemma ex_point_lg_out : forall l A P, A <> P -> Q_Cong l -> ~ Q_Cong_Null l -> exists B, l A B /\ Out A B P.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    assert(HH:= H0).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    unfold Q_Cong in HH.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    ex_and HH X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    ex_and H2 Y.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    assert(HP:= H3 X Y).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HP.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    assert(l X Y).
(* Goal: False *)
      apply H2.
(* Goal: @Cong Tn X Y X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
      apply cong_reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    assert(X <> Y).
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
      intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      subst Y.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      apply H1.
(* Goal: @Q_Cong_Null Tn l *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      unfold Q_Cong_Null.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
      split.
(* Goal: l1 A0 B0 *)
        auto.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => l A A) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
      exists X.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    assert(HH:= segment_construction_3 A P X Y H H6).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (@Out Tn A B P)) *)
    ex_and HH B.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
    exists B.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: l A B *)
(* Goal: @Out Tn A B P *)
      assert(HH:= H3 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
      destruct HH.
(* Goal: l A B *)
(* Goal: @Out Tn A B P *)
      apply H9.
(* Goal: @Cong Tn A B A B *)
      Cong.
(* Goal: @Out Tn A B P *)
    apply l6_6.
(* Goal: l1 A0 B0 *)
    auto.
Qed.

Lemma ex_point_lg_bet : forall l A M, Q_Cong l -> exists B : Tpoint, l M B /\ Bet A M B.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @EqL Tn l1 l2 *)
    assert(HH:= H).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    unfold Q_Cong in HH.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    ex_and HH X.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    ex_and H0 Y.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    assert(HP:= H1 X Y).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
    destruct HP.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    assert(l X Y).
(* Goal: iff (l1 X Y) (l2 X Y) *)
      apply H0.
(* Goal: @Cong Tn X Y X Y *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
      apply cong_reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l M B) (@Bet Tn A M B)) *)
    prolong A M B X Y.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
    exists B.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
    split; auto.
(* Goal: @Cong Tn A B A B *)
    eapply (lg_cong_lg l X Y); Cong.
Qed.

End Length_2.

Ltac lg_instance1 l A B :=
  assert(tempo_sg:= ex_point_lg l);
  match goal with
    |H: Q_Cong l |-  _ => assert(tempo_H:=H); apply (tempo_sg A) in tempo_H; ex_elim tempo_H B; exists B
  end;
  clear tempo_sg.

(* TODO : translate this kind of notations *)
Tactic Notation "soit" ident(A) ident(B) "de" "longueur" ident(l) := lg_instance1 l A B.

Ltac lg_instance2 l A P B :=
  assert(tempo_sg:= ex_point_lg_out l);
  match goal with
    |H: A <> P |-  _ =>
                        match goal with
                           |HP : Q_Cong l |-  _ =>
                                               match goal with
                                                 |HQ : ~ Q_Cong_Null l |-  _ => assert(tempo_HQ:=HQ);
                                                                           apply (tempo_sg A P H HP) in tempo_HQ;
                                                                           ex_and tempo_HQ B
                                               end
                        end
  end;
  clear tempo_sg.


Tactic Notation "soit" ident(B) "sur" "la" "demie" "droite" ident(A) ident(P) "/" "longueur" ident(A) ident(B) "=" ident(l) := lg_instance2 l A P B.

Section Length_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma ex_points_lg_not_col : forall l P, Q_Cong l -> ~ Q_Cong_Null l -> exists A, exists B, l A B /\ ~Col A B P.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P)))) *)
    assert(HH:=another_point P).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P)))) *)
    ex_elim HH A.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P)))) *)
    assert(HH:= not_col_exists P A H1).
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P)))) *)
    ex_elim HH Q.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P))) *)
    assert(A <> Q).
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
      intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P))) *)
      subst Q.
(* Goal: False *)
      apply H2.
(* Goal: @Col Tn P A A *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P))) *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l A B) (not (@Col Tn A B P))) *)
    lg_instance2 l A Q B.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
    exists B.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    intro.
(* Goal: False *)
    apply H2.
(* Goal: @Col Tn P A Q *)
    assert(A <> B).
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn P A Q *)
      subst B.
(* Goal: False *)
(* Goal: @Col Tn P A Q *)
      unfold Out in H5.
(* Goal: False *)
(* Goal: @Col Tn P A Q *)
      tauto; apply out_col in H5.
(* Goal: @Col Tn P A Q *)
    apply out_col in H5.
(* Goal: @Col Tn P A Q *)
    ColR.
Qed.

End Length_3.

Ltac lg_instance_not_col l P A B :=
  assert(tempo_sg:= ex_points_lg_not_col l P);
  match goal with
        |HP : Q_Cong l |-  _ => match goal with
                                  |HQ : ~ Q_Cong_Null l |-  _ => assert(tempo_HQ:=HQ);
                                                            apply (tempo_sg HP) in tempo_HQ;
                                                            elim tempo_HQ;
                                                            intro A;
                                                            let tempo_HR := fresh "tempo_HR" in
                                                            intro tempo_HR;
                                                            elim tempo_HR;
                                                            intro B;
                                                            intro;
                                                            spliter;
                                                            clear tempo_HR tempo_HQ
                            end
  end;
  clear tempo_sg.



Tactic Notation "soit" ident(B) "sur" "la" "demie" "droite" ident(A) ident(P) "/" "longueur" ident(A) ident(B) "=" ident(l) := lg_instance2 l A P B.

Require Import Setoid.

Section Length_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Notation "l1 =l= l2" := (EqL l1 l2) (at level 80, right associativity).

Lemma ex_eql : forall l1 l2, (exists A , exists B, Len A B l1 /\ Len A B l2)  -> l1 =l= l2.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H A.
(* Goal: @EqL Tn l1 l2 *)
    ex_and H0 B.
(* Goal: @EqL Tn l1 l2 *)
    assert(HH:=H).
(* Goal: @EqL Tn l1 l2 *)
    assert(HH0:=H0).
(* Goal: @EqL Tn l1 l2 *)
    unfold Len in HH.
(* Goal: @EqL Tn l1 l2 *)
    unfold Len in HH0.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: @EqL Tn l1 l2 *)
    unfold EqL.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
    repeat split; auto.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
      intro.
(* Goal: l1 A0 B0 *)
      assert(Len A0 B0 l1).
(* Goal: @Len Tn A0 B0 l2 *)
(* Goal: l1 A0 B0 *)
        unfold Len.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
        split; auto.
(* Goal: l1 A0 B0 *)
      assert(Cong A B A0 B0).
(* Goal: l1 A0 B0 *)
        apply (is_len_cong _ _ _ _ l1); auto.
(* Goal: l1 A0 B0 *)
      assert(Len A0 B0 l2).
(* Goal: @Len Tn A0 B0 l1 *)
(* Goal: l1 A0 B0 *)
        apply(is_len_cong_is_len A B).
(* Goal: iff (l1 X Y) (l2 X Y) *)
          apply H0.
(* Goal: l1 A0 B0 *)
        auto.
(* Goal: l1 A0 B0 *)
      unfold Len in H8.
(* Goal: l1 A0 B0 *)
      spliter.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
    intro.
(* Goal: l1 A0 B0 *)
    assert(Len A0 B0 l2).
(* Goal: @Len Tn A0 B0 l2 *)
(* Goal: l1 A0 B0 *)
      unfold Len.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
      split; auto.
(* Goal: l1 A0 B0 *)
    assert(Cong A B A0 B0).
(* Goal: l1 A0 B0 *)
      apply (is_len_cong _ _ _ _ l2); auto.
(* Goal: l1 A0 B0 *)
    assert(Len A0 B0 l1).
(* Goal: @Len Tn A0 B0 l1 *)
(* Goal: l1 A0 B0 *)
      apply(is_len_cong_is_len A B).
(* Goal: @Len Tn A A la *)
(* Goal: @Len Tn A A lb *)
        apply H.
(* Goal: l1 A0 B0 *)
      auto.
(* Goal: l1 A0 B0 *)
    unfold Len in H8.
(* Goal: l1 A0 B0 *)
    spliter.
(* Goal: l1 A0 B0 *)
    auto.
Qed.


Lemma all_eql : forall A B l1 l2, Len A B l1 -> Len A B l2 -> EqL l1 l2.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @EqL Tn l1 l2 *)
    apply ex_eql.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
    exists A.
(* Goal: @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B0 X Y) (@Cong Tn A B X Y)) *)
(* Goal: @Cong Tn A B A B *)
    exists B.
(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
    split; auto.
Qed.



Lemma null_len : forall A B la lb, Len A A la -> Len B B lb -> EqL la lb.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @EqL Tn la lb *)
    eapply (all_eql A A).
(* Goal: @Len Tn A A la *)
(* Goal: @Len Tn A A lb *)
      apply H.
(* Goal: @Cong Tn A B A B *)
    eapply (is_len_cong_is_len B B); Cong.
Qed.

Global Instance eqL_equivalence : Equivalence EqL.
Proof.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
split.
- unfold Reflexive.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
  intros.
(* Goal: @EqL Tn l1 l2 *)
  unfold EqL.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
  intros.
(* Goal: l1 A0 B0 *)
  tauto.
- unfold Symmetric.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
  intros.
(* Goal: @Q_Cong Tn l2 *)
  unfold EqL in *.
(* Goal: forall A B : @Tpoint Tn, iff (y A B) (x A B) *)
  firstorder.
- unfold Transitive.
(* Goal: @EqL Tn l1 l2 *)
  unfold EqL.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
  intros.
(* Goal: iff (x A B) (z A B) *)
  rewrite H.
(* Goal: iff (l1 X Y) (l2 X Y) *)
  apply H0.
Qed.


Lemma ex_lg : forall A B, exists l, Q_Cong l /\ l A B.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @ex (forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (fun l : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop => and (@Q_Cong Tn l) (l A B)) *)
    exists (fun C D => Cong A B C D).
(* Goal: and (@Q_Cong Tn (fun C D : @Tpoint Tn => @Cong Tn A B C D)) (@Cong Tn A B A B) *)
    unfold Q_Cong.
(* Goal: and (@ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y)))) (@Cong Tn A B A B) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun A0 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B0 : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A0 B0 X Y) (@Cong Tn A B X Y))) *)
(* Goal: @Cong Tn A B A B *)
      exists A. exists B.
(* Goal: l1 A0 B0 *)
      tauto.
(* Goal: @Cong Tn A B A B *)
    Cong.
Qed.

Lemma lg_eql_lg : forall l1 l2, Q_Cong l1 -> EqL l1 l2 -> Q_Cong l2.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: @Q_Cong Tn l2 *)
    unfold EqL in *.
(* Goal: @Q_Cong Tn l2 *)
    unfold Q_Cong in *.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B X Y) (l2 X Y))) *)
    decompose [ex] H.
(* Goal: @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => forall X Y : @Tpoint Tn, iff (@Cong Tn A B X Y) (l2 X Y))) *)
    exists x. exists x0.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
    intros.
(* Goal: iff (@Cong Tn x x0 X Y) (l2 X Y) *)
    rewrite H2.
(* Goal: iff (l1 X Y) (l2 X Y) *)
    apply H0.
Qed.

Lemma ex_eqL : forall l1 l2, Q_Cong l1 -> Q_Cong l2 -> (exists A, exists B, l1 A B /\ l2 A B) -> EqL l1 l2.
Proof.
(* Goal: forall (l1 l2 : forall (_ : @Tpoint Tn) (_ : @Tpoint Tn), Prop) (_ : @Q_Cong Tn l1) (_ : @Q_Cong Tn l2) (_ : @ex (@Tpoint Tn) (fun A : @Tpoint Tn => @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (l1 A B) (l2 A B)))), @EqL Tn l1 l2 *)
intros.
(* Goal: @EqL Tn l1 l2 *)
ex_and H1 A.
(* Goal: @EqL Tn l1 l2 *)
ex_and H2 B.
(* Goal: @EqL Tn l1 l2 *)
unfold EqL.
(* Goal: forall A B : @Tpoint Tn, iff (l1 A B) (l2 A B) *)
assert(HH1:= H).
(* Goal: forall A B : @Tpoint Tn, iff (l1 A B) (l2 A B) *)
assert(HH2:= H0).

(* Goal: forall A B : @Tpoint Tn, iff (l1 A B) (l2 A B) *)
unfold Q_Cong in HH1.
(* Goal: forall A B : @Tpoint Tn, iff (l1 A B) (l2 A B) *)
unfold Q_Cong in HH2.
(* Goal: forall A B : @Tpoint Tn, iff (l1 A B) (l2 A B) *)
ex_and HH1 A1.
(* Goal: iff (l1 A0 B0) (l2 A0 B0) *)
ex_and H3 B1.
(* Goal: iff (l1 A0 B0) (l2 A0 B0) *)
ex_and HH2 A2.
(* Goal: iff (l1 A0 B0) (l2 A0 B0) *)
ex_and H3 B2.

(* Goal: and (@Len Tn A B l1) (@Len Tn A B l2) *)
repeat split; auto.
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
intro.
(* Goal: l1 A0 B0 *)
assert(HH:= H4 A0 B0).
(* Goal: l1 A0 B0 *)
assert(HP:= H5 A0 B0).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HP.
(* Goal: l1 A0 B0 *)
apply H6.
(* Goal: @Cong Tn A2 B2 A0 B0 *)
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
assert(HP:= H4 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
assert(HQ:= H5 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HP.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HQ.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H9 in H1.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H11 in H2.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HH.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H13 in H3.
(* Goal: @Cong Tn A2 B2 A0 B0 *)
(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
apply cong_transitivity with A B; trivial.
(* Goal: @Cong Tn A B A B *)
apply cong_transitivity with A1 B1; Cong.

(* Goal: forall _ : l2 A0 B0, l1 A0 B0 *)
intro.
(* Goal: l1 A0 B0 *)
assert(HH:= H4 A0 B0).
(* Goal: l1 A0 B0 *)
assert(HP:= H5 A0 B0).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HH.
(* Goal: l1 A0 B0 *)
apply H6.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
assert(HH:= H4 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
assert(HQ:= H5 A B).
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HH.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HQ.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H9 in H1.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H11 in H2.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
destruct HP.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply H13 in H3.
(* Goal: @Cong Tn A1 B1 A0 B0 *)
apply cong_transitivity with A2 B2; trivial.
(* Goal: @Cong Tn A B A B *)
apply cong_transitivity with A B; Cong.
Qed.


End Length_4.
