Require Export GeoCoq.Tarski_dev.Ch10_line_reflexivity_2.

Section PerpBisect_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma perp_bisect_equiv_def :
  forall P Q A B, Perp_bisect P Q A B <-> Perp_bisect_bis P Q A B.
Proof.
(* Goal: forall P Q A B : @Tpoint Tn, iff (@Perp_bisect Tn P Q A B) (@Perp_bisect_bis Tn P Q A B) *)
intros; unfold Perp_bisect; unfold Perp_bisect_bis; unfold ReflectL; split.

(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
  {
(* Goal: forall _ : and (and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B A) (@Col Tn P Q X))) (or (@Perp Tn P Q B A) (@eq (@Tpoint Tn) B A))) (not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Perp_at Tn I P Q A B) (@Midpoint Tn I A B)) *)
  intro H; destruct H as [[[X [HMid HCol]] HPerp] HDiff].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Perp_at Tn I P Q A B) (@Midpoint Tn I A B)) *)
  exists X; split; Midpoint.
(* Goal: @Perp_at Tn X P Q A B *)
  elim HPerp; clear HPerp; intro HPerp; intuition.
(* Goal: @Perp_at Tn X P Q A B *)
  apply l8_14_2_1b_bis; assert_cols; Col; Perp.
  }

(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
  {
(* Goal: forall _ : @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Perp_at Tn I P Q A B) (@Midpoint Tn I A B)), and (and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B A) (@Col Tn P Q X))) (or (@Perp Tn P Q B A) (@eq (@Tpoint Tn) B A))) (not (@eq (@Tpoint Tn) A B)) *)
  intro H; destruct H as [I [HPerp HMid]].
(* Goal: and (and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B A) (@Col Tn P Q X))) (or (@Perp Tn P Q B A) (@eq (@Tpoint Tn) B A))) (not (@eq (@Tpoint Tn) A B)) *)
  assert_diffs; split; Col.
(* Goal: and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B A) (@Col Tn P Q X))) (or (@Perp Tn P Q B A) (@eq (@Tpoint Tn) B A)) *)
  split; try (left; apply l8_14_2_1a with I); Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X B A) (@Col Tn P Q X)) *)
  exists I; split; Midpoint.
(* Goal: @Col Tn P Q I *)
  unfold Perp_at in *; spliter; Col.
  }
Qed.

Lemma perp_bisect_sym_1 :
 forall P Q A B,
  Perp_bisect P Q A B ->
  Perp_bisect Q P A B.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Cong Tn A Q B Q *)
apply perp_bisect_equiv_def in H.
(* Goal: @Perp_bisect Tn P Q A B *)
apply perp_bisect_equiv_def.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
elim H;intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X P Q A B) *)
exists x.
(* Goal: and (@Perp_at Tn x P Q B A) (@Midpoint Tn x B A) *)
intuition; Perp.
Qed.

Lemma perp_bisect_sym_2 :
 forall P Q A B,
  Perp_bisect P Q A B ->
  Perp_bisect P Q B A.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Cong Tn A Q B Q *)
apply perp_bisect_equiv_def in H.
(* Goal: @Perp_bisect Tn P Q A B *)
apply perp_bisect_equiv_def.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
elim H;intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X P Q A B) *)
exists x.
(* Goal: and (@Perp_at Tn x P Q B A) (@Midpoint Tn x B A) *)
intuition; Perp.
Qed.

Lemma perp_bisect_sym_3 : forall A B C D,
 Perp_bisect A B C D ->
 Perp_bisect B A D C.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Perp_bisect Tn B A D C *)
apply perp_bisect_sym_1.
(* Goal: @Perp_bisect Tn A B D C *)
apply perp_bisect_sym_2.
(* Goal: @Perp_bisect Tn A B C D *)
trivial.
Qed.

Lemma perp_bisect_perp :
 forall P Q A B,
  Perp_bisect P Q A B ->
  Perp P Q A B.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Cong Tn A Q B Q *)
apply perp_bisect_equiv_def in H.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
(* Goal: @Perp Tn P Q A B *)
decompose [and ex] H;clear H.
(* Goal: @Perp Tn P Q A B *)
unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X P Q A B) *)
exists x.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
assumption.
Qed.

End PerpBisect_1.

Hint Resolve perp_bisect_perp : perp.

Section PerpBisect_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma perp_bisect_cong_1 :
 forall P Q A B,
 Perp_bisect P Q A B ->
 Cong A P B P.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Cong Tn A Q B Q *)
apply perp_bisect_equiv_def in H.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
(* Goal: @Cong Tn A Q B Q *)
elim H;intros I;intros;clear H.
(* Goal: @Cong Tn A Q B Q *)
decompose [and] H0;clear H0.
(* Goal: @Cong Tn A P B P *)
assert (Cong P A P B).
apply (per_double_cong P I A B);
eauto with perp.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
Cong.
Qed.

Lemma perp_bisect_cong_2 :
 forall P Q A B,
 Perp_bisect P Q A B ->
 Cong A Q B Q.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Cong Tn A Q B Q *)
apply perp_bisect_equiv_def in H.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
(* Goal: @Cong Tn A Q B Q *)
elim H;intros I;intros;clear H.
(* Goal: @Cong Tn A Q B Q *)
decompose [and] H0;clear H0.
(* Goal: @Cong Tn A Q B Q *)
assert (Cong Q A Q B).
apply (per_double_cong Q I A B);
eauto with perp.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
Cong.
Qed.

End PerpBisect_2.

Hint Resolve perp_bisect_cong_1 perp_bisect_cong_2 : cong.

Section PerpBisect_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma perp_bisect_cong2 :
 forall P Q A B,
 Perp_bisect P Q A B ->
 Cong A P B P /\ Cong A Q B Q.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: and (and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B))) (and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q)) *)
split.
(* Goal: @Cong Tn A P B P *)
(* Goal: @Cong Tn A Q B Q *)
eauto using perp_bisect_cong_1.
(* Goal: @Cong Tn A Q B Q *)
eauto using perp_bisect_cong_2.
Qed.

Lemma perp_bisect_cong :
 forall A A1 B B1 C C1 O: Tpoint,
 ~ Col A B C ->
 Perp_bisect O A1 B C -> Perp_bisect O B1 A C -> Perp_bisect O C1 A B ->
 Cong A O B O -> Cong B O C O ->
 Cong A O C O.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply (cong_transitivity A O B O C O); assumption.
Qed.

Lemma cong_cop_perp_bisect :
 forall P Q A B,
 P <> Q -> A <> B ->
 Coplanar P Q A B ->
 Cong A P B P ->
 Cong A Q B Q ->
 Perp_bisect P Q A B.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Perp_bisect Tn P Q A B *)
apply perp_bisect_equiv_def.
(* Goal: @Perp_bisect_bis Tn P Q A B *)
unfold Perp_bisect_bis.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Perp_at Tn I P Q A B) (@Midpoint Tn I A B)) *)
elim (midpoint_existence A B).
(* Goal: forall (x : @Tpoint Tn) (_ : @Midpoint Tn x A B), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Perp_at Tn I P Q A B) (@Midpoint Tn I A B)) *)
intros I HI.
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
exists I.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
split;try assumption.
assert (Per P I A)
 by (unfold Per;exists B;eCong).

(* Goal: @Perp_at Tn I P Q A B *)
show_distinct A I.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
unfold Midpoint in *.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
spliter.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
treat_equalities.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
intuition.

(* Goal: @Perp_at Tn I P Q A B *)
show_distinct B I.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
unfold Midpoint in *.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
spliter.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
treat_equalities.
(* Goal: False *)
(* Goal: @Perp_at Tn I P Q A B *)
intuition.

(* Goal: @Perp_at Tn I P Q A B *)
induction(eq_dec_points P I).
(* Goal: @Perp_at Tn I P Q A B *)
(* Goal: @Perp_at Tn I P Q A B *)
subst.
(* Goal: @Perp_at Tn I I Q A B *)
(* Goal: @Perp_at Tn I P Q A B *)
eapply l8_13_2;Col.
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U I Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
(* Goal: @Perp_at Tn I P Q A B *)
exists Q. exists B;repeat split;Col.
(* Goal: @Per Tn Q I B *)
(* Goal: @Perp_at Tn I P Q A B *)
unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn P P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) P I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn P I V))))) *)
exists A.
(* Goal: and (and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B))) (and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q)) *)
split.
(* Goal: @Midpoint Tn I B A *)
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
Midpoint.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
Cong.

(* Goal: @Perp_at Tn I P Q A B *)
eapply l8_13_2.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
assumption.

(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply col_permutation_2.
(* Goal: @Col Tn P Q I *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply cop_per2__col with A; Col.
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
destruct(col_dec B A P).
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
exists I.
(* Goal: or (and (@Col Tn A P I) (@Col Tn Q I I)) (or (and (@Col Tn A Q I) (@Col Tn P I I)) (and (@Col Tn A I I) (@Col Tn P Q I))) *)
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
left.
(* Goal: and (@Col Tn A P I) (@Col Tn Q I I) *)
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
split; ColR.
(* Goal: @Coplanar Tn A P Q I *)
(* Goal: @Per Tn Q I A *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply coplanar_perm_12, col_cop__cop with B; Col; Cop.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
exists B; split; Cong.

(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply midpoint_col;auto.
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
exists P.
(* Goal: @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn P P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) P I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn P I V))))) *)
exists A.
(* Goal: and (@Col Tn P P Q) (and (@Col Tn A A B) (and (not (@eq (@Tpoint Tn) P I)) (and (not (@eq (@Tpoint Tn) A I)) (@Per Tn P I A)))) *)
repeat split;Col.
Qed.

Lemma perp_bisect_is_on_perp_bisect :
 forall A B C P,
  Is_on_perp_bisect P A B ->
  Is_on_perp_bisect P B C ->
  Is_on_perp_bisect P A C.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Is_on_perp_bisect Tn P A C *)
unfold Is_on_perp_bisect in *.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
eCong.
Qed.

Lemma perp_mid_perp_bisect : forall A B C D,
 Midpoint C A B -> Perp C D A B ->
 Perp_bisect C D A B.
Proof with finish.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : @Is_on_perp_bisect Tn P A B) (_ : @Is_on_perp_bisect Tn P B C), @Is_on_perp_bisect Tn P A C *)
intros.
(* Goal: @Perp_bisect Tn P Q A B *)
apply perp_bisect_equiv_def.
(* Goal: @Cong Tn A Q B Q *)
unfold Perp_bisect_bis in *.
exists C...
(* Goal: and (and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B))) (and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q)) *)
split...
assert_cols; apply l8_14_2_1b_bis...
Qed.

Lemma cong_cop2_perp_bisect_col : forall A B C D E,
  Coplanar A C D E ->
  Coplanar B C D E ->
  Cong C D C E ->
  Perp_bisect A B D E ->
  Col A B C.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @Coplanar Tn A C D E) (_ : @Coplanar Tn B C D E) (_ : @Cong Tn C D C E) (_ : @Perp_bisect Tn A B D E), @Col Tn A B C *)
intros A B C D E HCop1 HCop2 HCong1 HPerp.
(* Goal: @Col Tn A B C *)
assert (HCong2 := HPerp); apply perp_bisect_cong2 in HCong2; destruct HCong2 as [HCong2 Hc]; clear Hc.
(* Goal: @Col Tn A B C *)
apply perp_bisect_equiv_def in HPerp.
(* Goal: @Col Tn A B C *)
destruct HPerp as [F [HPerp [HBet HCong3]]].
(* Goal: @Col Tn A B C *)
assert (HDE : D <> E) by (assert_diffs; auto).
(* Goal: @Col Tn A B C *)
assert (HCol := HPerp); apply perp_in_col in HCol; destruct HCol as [HCol Hc]; clear Hc.
(* Goal: @Col Tn A B C *)
apply l8_14_2_1a in HPerp.
(* Goal: @Col Tn A B C *)
elim (eq_dec_points A C); intro; try (subst; Col).
(* Goal: @Col Tn A B C *)
apply cop_perp2__col with D E; Perp; Cop.
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
apply perp_bisect_perp; apply cong_cop_perp_bisect; Cong.
Qed.

Lemma perp_bisect_cop2_existence : forall A B C,
  A <> B -> exists P, exists Q, Perp_bisect P Q A B /\ Coplanar A B C P /\ Coplanar A B C Q.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
intros A B C HDiff.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
destruct (midpoint_existence A B) as [M HM].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
destruct (ex_perp_cop A B M C HDiff) as [Q []].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
exists M; exists Q; unfold Perp_bisect.
(* Goal: and (and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B))) (and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q)) *)
repeat split; Cop.
(* Goal: @Midpoint Tn I B A *)
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
  exists M; split; Col; Midpoint.
(* Goal: or (@Perp Tn M Q B A) (@eq (@Tpoint Tn) B A) *)
  left; Perp.
Qed.

Lemma perp_bisect_existence :
  forall A B, A <> B -> exists P, exists Q, Perp_bisect P Q A B.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp_bisect Tn P Q A B)) *)
intros A B HDiff.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp_bisect Tn P Q A B)) *)
destruct (perp_bisect_cop2_existence A B A HDiff) as [P [Q []]].
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
exists P; exists Q; assumption.
Qed.

Lemma perp_bisect_existence_cop : forall A B C,
  A <> B -> exists P, exists Q, Perp_bisect P Q A B /\ Coplanar A B C P /\
                                Coplanar A B C Q.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
intros A B C HDiff.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
destruct (midpoint_existence A B) as [M HM].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
destruct (ex_perp_cop A B M C) as [Q [HQ HCop]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp_bisect Tn P Q A B) (and (@Coplanar Tn A B C P) (@Coplanar Tn A B C Q)))) *)
exists M; exists Q; unfold Perp_bisect.
(* Goal: and (and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B))) (and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q)) *)
split.

(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
  {
(* Goal: and (@ReflectL Tn A B M Q) (not (@eq (@Tpoint Tn) A B)) *)
  split; Col.
(* Goal: @ReflectL Tn A B M Q *)
  split; Perp.
(* Goal: @Midpoint Tn I B A *)
(* Goal: @Cong Tn Q B Q A *)
(* Goal: @Perp_at Tn I P Q A B *)
  exists M; split; Col; Midpoint.
  }

(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
  {
(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
  split; auto.
(* Goal: @Coplanar Tn A B C M *)
  assert (Coplanar A B Q M) by Cop.
(* Goal: @Coplanar Tn A B C M *)
  apply perp_not_col2 in HQ.
(* Goal: @Coplanar Tn A B C M *)
  elim HQ; clear HQ; intro; [CopR|].
(* Goal: @Coplanar Tn A B C M *)
  assert_cols; exfalso; Col.
  }
Qed.

End PerpBisect_3.

Section PerpBisect_2D.

(* Goal: and (@Coplanar Tn A B C M) (@Coplanar Tn A B C Q) *)
Context `{T2D:Tarski_2D}.

Lemma cong_perp_bisect :
 forall P Q A B,
 P <> Q -> A <> B ->
 Cong A P B P ->
 Cong A Q B Q ->
 Perp_bisect P Q A B.
Proof.
(* Goal: forall (P Q A B : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Cong Tn A P B P) (_ : @Cong Tn A Q B Q), @Perp_bisect Tn P Q A B *)
intros P Q A B HPQ HAB.
(* Goal: forall (_ : @Cong Tn A P B P) (_ : @Cong Tn A Q B Q), @Perp_bisect Tn P Q A B *)
assert (HCop := all_coplanar P Q A B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @Col Tn I P Q *)
(* Goal: @Col Tn I A B *)
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U P Q) (and (@Col Tn V A B) (and (not (@eq (@Tpoint Tn) U I)) (and (not (@eq (@Tpoint Tn) V I)) (@Per Tn U I V)))))) *)
apply cong_cop_perp_bisect; assumption.
Qed.

Lemma cong_perp_bisect_col : forall A B C D E,
  Cong C D C E ->
  Perp_bisect A B D E ->
  Col A B C.
Proof.
(* Goal: forall (A B C D E : @Tpoint Tn) (_ : @Cong Tn C D C E) (_ : @Perp_bisect Tn A B D E), @Col Tn A B C *)
intros A B C D E.
(* Goal: forall (_ : @Cong Tn C D C E) (_ : @Perp_bisect Tn A B D E), @Col Tn A B C *)
apply cong_cop2_perp_bisect_col; apply all_coplanar.
Qed.

End PerpBisect_2D.