Require Import GeoCoq.Tarski_dev.Ch08_orthogonality.
Require Import Relations.

Section Grad.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma grad__bet : forall A B C, Grad A B C -> Bet A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Grad Tn A B C) (_ : not (@eq (@Tpoint Tn) A C)), not (@eq (@Tpoint Tn) A B) *)
  intros A B C HG.
(* Goal: @Bet Tn A B C *)
  elim HG; clear HG A B C; [Between|eBetween].
Qed.

Lemma grad__col : forall A B C, Grad A B C -> Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Grad Tn A B C), @Col Tn A B C *)
  intros; apply bet_col, grad__bet; assumption.
Qed.

Lemma grad_neq__neq13 : forall A B C, Grad A B C -> A <> B -> A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Grad Tn A B C) (_ : not (@eq (@Tpoint Tn) A B)), not (@eq (@Tpoint Tn) A C) *)
  intros A B C HG HAB Heq.
(* Goal: False *)
  subst C.
(* Goal: False *)
  apply HAB.
(* Goal: @eq (@Tpoint Tn) A B *)
  apply between_identity, grad__bet; trivial.
Qed.

Lemma grad_neq__neq12 : forall A B C, Grad A B C -> A <> C -> A <> B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Grad Tn A B C) (_ : not (@eq (@Tpoint Tn) A C)), not (@eq (@Tpoint Tn) A B) *)
  intros A B C HG.
(* Goal: forall _ : not (@eq (@Tpoint Tn) A C), not (@eq (@Tpoint Tn) A B) *)
  elim HG; clear HG A B C; intros; intro; treat_equalities.
(* Goal: False *)
(* Goal: False *)
    auto.
(* Goal: False *)
(* Goal: False *)
  apply H0; auto.
Qed.

Lemma grad112__eq : forall A B, Grad A A B -> A = B.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : @Grad Tn A B A), @eq (@Tpoint Tn) A B *)
  intros A B HG.
(* Goal: @eq (@Tpoint Tn) A B *)
  assert (HA' : exists A', A' = A /\ Grad A A' B) by (exists A; auto).
(* Goal: @eq (@Tpoint Tn) A B *)
  destruct HA' as [A' [Heq HG']].
(* Goal: @eq (@Tpoint Tn) A B *)
  clear HG.
(* Goal: @eq (@Tpoint Tn) A B *)
  revert Heq.
(* Goal: False *)
(* Goal: False *)
  elim HG'; auto.
(* Goal: forall (A B C C' : @Tpoint Tn) (_ : @Grad Tn A B C) (_ : forall _ : @eq (@Tpoint Tn) B A, @eq (@Tpoint Tn) A C) (_ : @Bet Tn A C C') (_ : @Cong Tn A B C C') (_ : @eq (@Tpoint Tn) B A), @eq (@Tpoint Tn) A C' *)
  clear HG' A B A'.
(* Goal: False *)
(* Goal: False *)
  intros; treat_equalities; auto.
Qed.

Lemma grad121__eq : forall A B, Grad A B A -> A = B.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : @Grad Tn A B A), @eq (@Tpoint Tn) A B *)
  intros A B HG.
(* Goal: @eq (@Tpoint Tn) A B *)
  apply between_identity, grad__bet; trivial.
Qed.

Lemma grad__le : forall A B C, Grad A B C -> Le A B A C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, iff (@GradExp Tn A B C) (GradExpInv A B C) *)
  intros.
(* Goal: @Le Tn A B A C *)
  apply grad__bet in H.
(* Goal: False *)
(* Goal: False *)
  apply l5_12_a in H; spliter; auto.
Qed.

Lemma grad2__grad123 : forall A B C D E F, Grad2 A B C D E F -> Grad A B C.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @GradExp2 Tn A B C D E F), @GradExp Tn D E F *)
  intros A B C D E F.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @Grad Tn A B B *)
(* Goal: @Grad Tn A B C' *)
    apply grad_init.
(* Goal: False *)
(* Goal: False *)
    apply (grad_stab _ _ C); auto.
Qed.

Lemma grad2__grad456 : forall A B C D E F, Grad2 A B C D E F -> Grad D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @GradExp2 Tn A B C D E F), @GradExp Tn D E F *)
  intros A B C D E F.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @Grad Tn A B B *)
(* Goal: @Grad Tn A B C' *)
    apply grad_init.
(* Goal: False *)
(* Goal: False *)
    apply (grad_stab _ _ F); auto.
Qed.

Lemma grad_sum : forall A B C D E,
  Grad A B C -> Grad A B D -> Bet A C E -> Cong A D C E ->
  Grad A B E.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @Grad Tn A B C) (_ : @Grad Tn A B D) (_ : @Bet Tn A C E) (_ : @Cong Tn A D C E), @Grad Tn A B E *)
  intros A B C D E HGC HGD.
(* Goal: forall (_ : @Bet Tn A C E) (_ : @Cong Tn A D C E), @Grad Tn A B E *)
  elim (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  { intros; subst B.
(* Goal: @Grad Tn A A E *)
    assert(A = C) by (apply grad112__eq; trivial).
(* Goal: @Grad Tn A A E *)
    assert(A = D) by (apply grad112__eq; trivial).
(* Goal: @Grad Tn A A E *)
    treat_equalities; trivial.
  }
(* Goal: forall (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Bet Tn A C E) (_ : @Cong Tn A D C E), @Grad Tn A B E *)
  intro HAB.
(* Goal: forall (_ : @Bet Tn A C E) (_ : @Cong Tn A D C E), @Grad Tn A B E *)
  revert E.
(* Goal: forall (E : @Tpoint Tn) (_ : @Bet Tn A C E) (_ : @Cong Tn A D C E), @Grad Tn A B E *)
  induction HGD.
(* Goal: forall (E : @Tpoint Tn) (_ : @Bet Tn A C E) (_ : @Cong Tn A B C E), @Grad Tn A B E *)
(* Goal: forall (E : @Tpoint Tn) (_ : @Bet Tn A C E) (_ : @Cong Tn A C' C E), @Grad Tn A B E *)
    intro E; apply grad_stab; trivial.
(* Goal: forall (E : @Tpoint Tn) (_ : @Bet Tn A C E) (_ : @Cong Tn A C' C E), @Grad Tn A B E *)
  rename C0 into D; rename C' into D'.
(* Goal: forall (E : @Tpoint Tn) (_ : @Bet Tn A C E) (_ : @Cong Tn A D' C E), @Grad Tn A B E *)
  intros E' HBet' HCong'.
(* Goal: @Grad Tn A B E' *)
  destruct(segment_construction A C A D) as [E [HBet HCong]].
(* Goal: @Grad Tn A B E' *)
  assert (HBet1 : Bet A B C) by (apply grad__bet; trivial).
(* Goal: @Grad Tn A B E' *)
  assert (HBet2 : Bet A B D) by (apply grad__bet; trivial).
(* Goal: @Grad Tn A B E' *)
  assert(HBet3 : Bet C E E').
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  { apply l6_13_1.
(* Goal: @Out Tn C E E' *)
(* Goal: @Le Tn C E C E' *)
      assert_diffs; apply l6_2 with A; Between.
(* Goal: @Le Tn C E C E' *)
    apply (l5_6 A D A D'); Cong.
(* Goal: @Le Tn A D A D' *)
    apply bet__le1213; trivial.
  }
(* Goal: @Grad Tn A B E' *)
  apply grad_stab with E; auto with cong; eBetween.
(* Goal: False *)
(* Goal: False *)
  apply cong_transitivity with D D'; auto.
(* Goal: @Cong Tn D D' E E' *)
  apply l4_3_1 with A C; Cong.
Qed.

Lemma gradexp__grad : forall A B C, GradExp A B C -> Grad A B C.
Proof.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @Grad Tn A B B *)
(* Goal: @Grad Tn A B C' *)
    apply grad_init.
(* Goal: False *)
(* Goal: False *)
  apply grad_sum with C C; auto.
Qed.

Lemma gradexp_le__reach : forall A B C D B',
  GradExp A B B' -> Le C D A B' ->
  Reach A B C D.
Proof.
(* Goal: forall (A B C D B' : @Tpoint Tn) (_ : @GradExp Tn A B B') (_ : @Le Tn C D A B'), @Reach Tn A B C D *)
  intros A B C D B' HGE HLe.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@GradExp Tn A B B') (@Le Tn C D A B')) *)
  exists B'; split; trivial.
(* Goal: @Grad Tn A B B' *)
  apply gradexp__grad; trivial.
Qed.

Lemma grad__ex_gradexp_le : forall A B C,
  Grad A B C ->
  exists D, GradExp A B D /\ Le A C A D.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Grad Tn A B C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A C A D)) *)
  intros A B C.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A B A D)) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A C' A D)) *)
    exists B; split; Le; apply gradexp_init.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A C' A D)) *)
  destruct IHGrad as [D [HGE HLe]].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A C' A D)) *)
  destruct (segment_construction A D A D) as [D' [HBet HCong]].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@GradExp Tn A B D) (@Le Tn A C' A D)) *)
  exists D'; split.
(* Goal: @GradExp Tn A B D' *)
(* Goal: @Le Tn A C' A D' *)
    apply gradexp_stab with D; Cong.
(* Goal: @Le Tn A C' A D' *)
  apply bet2_le2__le1346 with C D; Le.
(* Goal: @Le Tn C C' D D' *)
  apply gradexp__grad, grad__bet in HGE.
(* Goal: @Le Tn C C' D D' *)
  apply l5_6 with A B A D; Cong; Le.
Qed.

Lemma reach__ex_gradexp_le : forall A B C D, Reach A B C D ->
  exists B', GradExp A B B' /\ Le C D A B'.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Reach Tn A B C D), @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@GradExp Tn A B B') (@Le Tn C D A B')) *)
  intros A B C D HR.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@GradExp Tn A B B') (@Le Tn C D A B')) *)
  destruct HR as [B0 [HG HLe]].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@GradExp Tn A B B') (@Le Tn C D A B')) *)
  destruct (grad__ex_gradexp_le A B B0 HG) as [B' [HG2 HLe2]].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@GradExp Tn A B B') (@Le Tn C D A B')) *)
  exists B'; split; trivial.
(* Goal: @Le Tn C D A B' *)
  apply le_transitivity with A B0; trivial.
Qed.

Lemma gradexp2__gradexp123 : forall A B C D E F,
  GradExp2 A B C D E F ->
  GradExp A B C.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @GradExp2 Tn A B C D E F), @GradExp Tn D E F *)
  intros A B C D E F.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @GradExp Tn D E E *)
(* Goal: @GradExp Tn D E F' *)
    apply gradexp_init.
(* Goal: False *)
(* Goal: False *)
  apply (gradexp_stab _ _ C); auto.
Qed.

Lemma gradexp2__gradexp456 : forall A B C D E F,
  GradExp2 A B C D E F ->
  GradExp D E F.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @GradExp2 Tn A B C D E F), @GradExp Tn D E F *)
  intros A B C D E F.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  induction 1.
(* Goal: @GradExp Tn D E E *)
(* Goal: @GradExp Tn D E F' *)
    apply gradexp_init.
(* Goal: False *)
(* Goal: False *)
  apply (gradexp_stab _ _ F); auto.
Qed.


Inductive GradExpInv : Tpoint -> Tpoint -> Tpoint -> Prop :=
    gradexpinv_init : forall A B, GradExpInv A B B
  | gradexpinv_stab : forall A B B' C, Bet A B' B -> Cong A B' B' B -> GradExpInv A B C ->
                    GradExpInv A B' C.

Lemma gradexp_clos_trans : forall A B C, GradExp A B C <->
  clos_refl_trans_n1 Tpoint (fun X Y => Midpoint X A Y) B C.
Proof.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  intros; split; induction 1.
  - constructor.
  - apply Relation_Operators.rtn1_trans with C; [split|]; assumption.
  - constructor.
  - apply gradexp_stab with y; finish.
Qed.

Lemma gradexpinv_clos_trans : forall A B C, GradExpInv A B C <->
  clos_refl_trans_1n Tpoint (fun X Y => Midpoint X A Y) B C.
Proof.
(* Goal: forall _ : @GradExp2 Tn A B C D E F, @GradExp Tn D E F *)
  intros; split; induction 1.
  - constructor.
  - apply Relation_Operators.rt1n_trans with B; [split|]; assumption.
  - constructor.
  - apply gradexpinv_stab with y; finish.
Qed.

Lemma gradexp__gradexpinv : forall A B C, GradExp A B C <-> GradExpInv A B C.
Proof.
(* Goal: forall A B C : @Tpoint Tn, iff (@GradExp Tn A B C) (GradExpInv A B C) *)
  intros.
(* Goal: iff (@GradExp Tn A B C) (GradExpInv A B C) *)
  rewrite gradexp_clos_trans, gradexpinv_clos_trans.
  rewrite <- clos_rt_rt1n_iff, <- clos_rt_rtn1_iff.
(* Goal: iff (clos_refl_trans (@Tpoint Tn) (fun X Y : @Tpoint Tn => @Midpoint Tn X A Y) B C) (clos_refl_trans (@Tpoint Tn) (fun X Y : @Tpoint Tn => @Midpoint Tn X A Y) B C) *)
  reflexivity.
Qed.

(** D is the last graduation of AB before or equal to C, and E the first graduation after C *)
Lemma reach__grad_min : forall A B C, A <> B -> Bet A B C -> Reach A B A C ->
  exists D E, Bet A D C /\ Grad A B D /\ E <> C /\ Bet A C E /\ Bet A D E /\ Cong A B D E.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Bet Tn A B C) (_ : @Reach Tn A B A C), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  intros A B C HAB HBet HReach.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  destruct HReach as [D [HD1 HD2]].
  apply l6_13_1 in HD2;
    [|apply l6_7 with B; [apply l6_6|]; apply bet_out; auto; apply grad__bet, HD1].
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  revert dependent C.
(* Goal: forall (C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A C D), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  induction HD1.
(* Goal: False *)
    intros; assert (B = C) by (apply between_equality with A; Between); subst C.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D B) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E B)) (and (@Bet Tn A B E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
(* Goal: forall (C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A C C'), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
    destruct (segment_construction A B A B) as [C []].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
    assert_diffs.
(* Goal: GradExpInv A x x *)
    exists B, C; repeat split; finish; constructor.
(* Goal: forall (C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @Bet Tn A C C'), @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C)) (and (@Bet Tn A C E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  intros; destruct (l5_3 A C0 C C'); trivial.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C0) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C0)) (and (@Bet Tn A C0 E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C0) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C0)) (and (@Bet Tn A C0 E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
    apply IHHD1; assumption.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C0) (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C0)) (and (@Bet Tn A C0 E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
  destruct (eq_dec_points C' C0).
  - subst C0.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C') (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C')) (and (@Bet Tn A C' E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
    destruct (segment_construction A C' A B) as [C'' []].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn A D C') (and (@Grad Tn A B D) (and (not (@eq (@Tpoint Tn) E C')) (and (@Bet Tn A C' E) (and (@Bet Tn A D E) (@Cong Tn A B D E))))))) *)
    exists C', C''; repeat split; Cong.
(* Goal: @Grad Tn A B C' *)
    apply grad_stab with C; assumption.
  - exists C, C'; repeat split; assumption.
Qed.

Lemma reach__ex_gradexp_lt : forall A B P Q, A <> B -> Reach P Q A B ->
  exists C, GradExp A C B /\ Lt A C P Q.
Proof.
(* Goal: forall (A B P Q : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Reach Tn P Q A B), @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  intros A B P Q HAB HReach.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  apply reach__ex_gradexp_le in HReach.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  destruct HReach as [R [HR1 HR2]].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  generalize dependent B.
(* Goal: forall A B C : @Tpoint Tn, iff (@GradExp Tn A B C) (GradExpInv A B C) *)
  induction HR1; rename A0 into P, B into Q; intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  { destruct (midpoint_existence A B) as [C []].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
    exists C; split.
(* Goal: @GradExp Tn A C B *)
(* Goal: @Lt Tn A C P Q *)
      rewrite gradexp__gradexpinv.
(* Goal: GradExpInv A x x *)
      apply gradexpinv_stab with B; auto; constructor.
(* Goal: @Lt Tn A C P Q *)
    apply le3456_lt__lt with A B; trivial.
(* Goal: @Lt Tn A C A B *)
    split; Le.
(* Goal: not (@Cong Tn A C A B) *)
    intro; assert (C = B) by (apply (between_cong A); assumption).
(* Goal: False *)
(* Goal: False *)
    treat_equalities; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  rename C into R, C' into R'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  destruct (midpoint_existence A B) as [M HM].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  assert_diffs.
(* Goal: False *)
(* Goal: False *)
  destruct (IHHR1 M) as [C []]; auto.
(* Goal: @Le Tn A M P R *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
    apply le_mid2__le12 with B R'; [|split|]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@GradExp Tn A C B) (@Lt Tn A C P Q)) *)
  exists C; split; trivial.
(* Goal: @GradExp Tn A C B *)
  destruct HM.
(* Goal: @GradExp Tn A C B *)
  apply gradexp_stab with M; trivial.
Qed.

End Grad.

Hint Resolve grad__bet : between.
Hint Resolve grad__col : col.