Require Export GeoCoq.Tarski_dev.Ch16_coordinates.

Section PythagoreanFun.

Context `{T2D:Tarski_2D}.
Context `{TE:@Tarski_euclidean Tn TnEQD}.

Lemma Ps_Col : forall O E A, Ps O E A -> Col O E A.
Proof.
(* Goal: forall (O E E' A B C1 C2 : @Tpoint Tn) (_ : @PythRel Tn O E E' A B C1) (_ : @PythRel Tn O E E' A B C2) (_ : or (and (@Ps Tn O E C1) (@Ps Tn O E C2)) (@eq (@Tpoint Tn) C1 O)), @eq (@Tpoint Tn) C1 C2 *)
intros.
(* Goal: @Col Tn O E A *)
unfold Ps in H.
(* Goal: @Col Tn O E A *)
apply out_col in H;Col.
Qed.

Lemma PythRel_exists : forall O E E', ~ Col O E  E' -> forall A B,
 Col O E A -> Col O E B ->
 exists C, PythRel O E E' A B C.
Proof.
(* Goal: forall (O E E' A B C1 C2 : @Tpoint Tn) (_ : @PythRel Tn O E E' A B C1) (_ : @PythRel Tn O E E' A B C2) (_ : or (and (@Ps Tn O E C1) (@Ps Tn O E C2)) (@eq (@Tpoint Tn) C1 O)), @eq (@Tpoint Tn) C1 C2 *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @PythRel Tn O E E' A B C) *)
assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @PythRel Tn O E E' A B C) *)
destruct (eq_dec_points O B).
- subst.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' A O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
 exists A.
(* Goal: @PythRel Tn O E E' A B C *)
 unfold PythRel.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
 split.
(* Goal: @Ar2 Tn B E E' A B A *)
(* Goal: or (and (@eq (@Tpoint Tn) B B) (or (@eq (@Tpoint Tn) A A) (@Opp Tn B E E' A A))) (@ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn B B' B B) (and (@Cong Tn B B' B B) (@Cong Tn B A A B')))) *)
 unfold Ar2;auto.
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
 left;auto.
-
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @PythRel Tn O E E' A B C) *)
destruct (perp_exists O E O) as [X HX].
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @PythRel Tn O E E' A B C) *)
destruct (segment_construction_2 X O O B) as [B' [HB1 HB2]].
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert_diffs;auto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @PythRel Tn O E E' A B C) *)
destruct (segment_construction_2 E O A B') as [C [HC1 HC2]].
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists C.
(* Goal: @PythRel Tn O E E' A B C *)
unfold PythRel.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split;auto.
(* Goal: @Col Tn O E C *)
(* Goal: or (and (@eq (@Tpoint Tn) O B) (or (@eq (@Tpoint Tn) A C) (@Opp Tn O E E' A C))) (@ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn O B' O B) (and (@Cong Tn O B' O B) (@Cong Tn O C A B')))) *)
destruct HC1.
(* Goal: @Col Tn O E C *)
(* Goal: @Col Tn O E C *)
(* Goal: or (and (@eq (@Tpoint Tn) O B) (or (@eq (@Tpoint Tn) A C) (@Opp Tn O E E' A C))) (@ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn O B' O B) (and (@Cong Tn O B' O B) (@Cong Tn O C A B')))) *)
auto using bet_col .
(* Goal: @Col Tn O E C *)
(* Goal: or (and (@eq (@Tpoint Tn) O B) (or (@eq (@Tpoint Tn) A C) (@Opp Tn O E E' A C))) (@ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn O B' O B) (and (@Cong Tn O B' O B) (@Cong Tn O C A B')))) *)
apply bet_col in H3. Col.
(* Goal: or (and (@eq (@Tpoint Tn) O B) (or (@eq (@Tpoint Tn) A C) (@Opp Tn O E E' A C))) (@ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn O B' O B) (and (@Cong Tn O B' O B) (@Cong Tn O C A B')))) *)
right.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => and (@Perp Tn O B' O B) (and (@Cong Tn O B' O B) (@Cong Tn O C A B'))) *)
exists B'.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.

(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
assert (Perp O X O B).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply (perp_col1 O X O E B);Col.
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Perp.
(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
assert (Perp O B O B').
(* Goal: @Perp Tn O B O B' *)
(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
 apply (perp_col1 O B O X B').
(* Goal: not (@eq (@Tpoint Tn) O B') *)
(* Goal: @Perp Tn O B O X *)
(* Goal: @Col Tn O X B' *)
(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
 intro;treat_equalities.
(* Goal: False *)
(* Goal: @Perp Tn O B O X *)
(* Goal: @Col Tn O X B' *)
(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
 intuition.
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
 Perp.
(* Goal: @Col Tn O X B' *)
(* Goal: @Perp Tn O B' O B *)
(* Goal: and (@Cong Tn O B' O B) (@Cong Tn O C A B') *)
 destruct HB1.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
 apply bet_col in H6. Col.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
 apply bet_col in H6. Col.
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
 Perp.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
 split.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
 Cong.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
 Cong.
Qed.

Lemma opp_same_square : forall O E E' A B A2, Opp O E E' A B -> Prod O E E' A A A2 -> Prod O E E' B B A2.
(* Goal: forall (O E E' A B C1 C2 : @Tpoint Tn) (_ : @PythRel Tn O E E' A B C1) (_ : @PythRel Tn O E E' A B C2) (_ : or (and (@Ps Tn O E C1) (@Ps Tn O E C2)) (@eq (@Tpoint Tn) C1 O)), @eq (@Tpoint Tn) C1 C2 *)
intros.

(* Goal: @Prod Tn O E E' B B A2 *)
assert(~Col O E E').
(* Goal: @Col Tn O E A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Prod in H0.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
unfold Ar2  in H0.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @Prod Tn O E E' B B A2 *)
assert(exists ME : Tpoint, Opp O E E' E ME).
apply(opp_exists O E E' H1 E); Col;
assert(HH:= opp_prod O E E').
(* Goal: @Prod Tn O E E' B B A2 *)
ex_and H2 ME.

(* Goal: @Prod Tn O E E' B B A2 *)
assert(HH:= opp_prod O E E' ME A B H3 H).
(* Goal: @Prod Tn O E E' B B A2 *)
assert(Prod O E E' B ME A).
(* Goal: @Prod Tn O E E' B ME A *)
(* Goal: @Prod Tn O E E' B B A2 *)
apply(opp_prod O E E' ME B A H3).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply opp_comm; auto.
(* Goal: @Prod Tn O E E' B B A2 *)
assert(Prod O E E' ME B A).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply prod_comm; auto.

(* Goal: @Prod Tn O E E' B B A2 *)
assert(HP:=(prod_assoc O E E' A ME B B A A2 HH H4)).
(* Goal: @Prod Tn O E E' B B A2 *)
destruct HP.
(* Goal: @Prod Tn O E E' B B A2 *)
apply H5.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
Qed.


(**********)

Lemma PythOK : forall O E E' A B C A2 B2 C2, PythRel O E E' A B C -> 
 Prod O E E' A A A2 ->
 Prod O E E' B B B2 ->
 Prod O E E' C C C2 ->
 Sum O E E' A2 B2 C2.
Proof.
(* Goal: forall (O E E' A B C1 C2 : @Tpoint Tn) (_ : @PythRel Tn O E E' A B C1) (_ : @PythRel Tn O E E' A B C2) (_ : or (and (@Ps Tn O E C1) (@Ps Tn O E C2)) (@eq (@Tpoint Tn) C1 O)), @eq (@Tpoint Tn) C1 C2 *)
intros.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold PythRel in H.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction H3.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(B2=O).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (prod_O_l_eq O E E' O); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B2.

(* Goal: @Sum Tn O E E' A2 O C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(A2 = C2).

(* Goal: @eq (@Tpoint Tn) A2 C2 *)
(* Goal: @Sum Tn O E E' A2 O C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction H7.

(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (prod_uniqueness O E E' A A); auto.
(* Goal: @eq (@Tpoint Tn) A2 C2 *)
(* Goal: @Sum Tn O E E' A2 O C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Prod O E E' C C A2).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_same_square O E E' A); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (prod_uniqueness O E E' C C); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C2.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (sum_A_O O E E' ); auto.
(* Goal: @Col Tn O E A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Prod in H0.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ar2 in H0; tauto.

(*
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H3 B'.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(B2=O).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (prod_O_l_eq O E E' O); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (sum_A_O O E E' ); auto.
(* Goal: @Col Tn O E A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Prod in H0.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ar2 in H0; tauto.
*)

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(O <> E).
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst E.
(* Goal: False *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply H.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H3 B'.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Per A O B').
(* Goal: @Per Tn A O B' *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply l8_2.
(* Goal: @Per Tn B' O A *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply (per_col _ _ B).
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_distinct in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Per Tn A O B1 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_in_per.
(* Goal: @Perp_at Tn O A O O B1 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn O O A B1 O *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_perp_in.
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Perp.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction(eq_dec_points A O).
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst A.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Cong O B O C).
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B'; Cong.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(B = C \/ Midpoint O B C).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l7_20; auto.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction H12.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(B2 = C2).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(prod_uniqueness O E E' B B); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C2.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(A2=O).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(prod_uniqueness O E E' O O); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply prod_0_l; auto.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst A2.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Col Tn O E B2 *)
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Prod in H2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E B2 *)
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(A2=O).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(prod_uniqueness O E E' O O); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply prod_0_l; auto.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst A2.
apply (midpoint_opp O E E') in H12;

unfold Midpoint in H12.
(* Goal: @Sum Tn O E E' O B2 C2 *)
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(C2 = B2).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(prod_uniqueness O E E' C C);auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (opp_same_square O E E' B C); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply sum_O_B; auto.
(* Goal: @Col Tn O E B2 *)
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Prod in H2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E B2 *)
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Ar2 Tn O E E' O B C *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction(out_dec O A E); induction(out_dec O B E);induction(out_dec O C E).

(****** A>0 ********* B>0 ********** C>0 ********)

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O A B C A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists C.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' A O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists A.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' B O D) (@Ps Tn O E D)) *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists B.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(****** A>0 ********* B>0 ********** C<0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OC : Tpoint, Opp O E E' C OC).
(* Goal: @ex (@Tpoint Tn) (fun OC : @Tpoint Tn => @Opp Tn O E E' C OC) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H C).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OC.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E C).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.

(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_symmetry in H9.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H9.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_right_comm in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_not_col in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply H3.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H14.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OC).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' C OC); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O A B OC A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O A *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ps in H16.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply out_col in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OC O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OC.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O C; Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' A O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists A.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' B O D) (@Ps Tn O E D)) *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists B.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' C OC C2 H16 H2).

(****** A>0 ********* B<0 ********** C>0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OB : Tpoint, Opp O E E' B OB).
(* Goal: @ex (@Tpoint Tn) (fun OB : @Tpoint Tn => @Opp Tn O E E' B OB) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H B).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OB.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E B).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H8.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_distinct in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H13.
(* Goal: @Bet Tn B O E *)
(* Goal: @Col Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
bet.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OB).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' B OB); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O A OB C A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply out_col in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists C.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' A O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists A.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
repeat split; Cong;
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OB O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OB.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B; Cong.
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_same_square O E E' B OB B2 H16 H1).

(****** A>0 ********* B<0 ********** C<0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OC : Tpoint, Opp O E E' C OC).
(* Goal: @ex (@Tpoint Tn) (fun OC : @Tpoint Tn => @Opp Tn O E E' C OC) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H C).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OC.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E C).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.

(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_symmetry in H9.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H9.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_right_comm in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_not_col in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply H3.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H14.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OC).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' C OC); auto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OB : Tpoint, Opp O E E' B OB).
(* Goal: @ex (@Tpoint Tn) (fun OB : @Tpoint Tn => @Opp Tn O E E' B OB) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H B).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H18 OB.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E B).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H8.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_distinct in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H13.
(* Goal: @Bet Tn B O E *)
(* Goal: @Col Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
bet.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OB).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' B OB); auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O A OB OC A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply out_col in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OC O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OC.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O C; Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' A O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists A.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
repeat split; Cong;
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OB O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OB.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B; Cong.
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_same_square O E E' B OB B2 H19 H1).
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' C OC C2 H16 H2).

(****** A<0 ********* B>0 ********** C>0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OA : Tpoint, Opp O E E' A OA).
(* Goal: @ex (@Tpoint Tn) (fun OA : @Tpoint Tn => @Opp Tn O E E' A OA) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H A).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OA.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E A).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply not_out_bet in H12;auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O OA B C A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists C.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Col O E OA).
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Opp in H16.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Sum in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E OA *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H16.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OA O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OA.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Out Tn O OA E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply not_out_bet in H12.
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(HP:=l5_2 A O E OA H11 H12 H16).
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Out.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
subst OA.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H18.
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
induction HP.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
right; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
left; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Opp in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O B *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Sum in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' B O D) (@Ps Tn O E D)) *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists B.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_same_square O E E' A OA A2 H16 H0).

(****** A<0 ********* B>0 ********** C<0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OC : Tpoint, Opp O E E' C OC).
(* Goal: @ex (@Tpoint Tn) (fun OC : @Tpoint Tn => @Opp Tn O E E' C OC) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H C).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OC.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E C).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.

(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_symmetry in H9.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H9.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_right_comm in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_not_col in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply H3.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H14.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OC).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' C OC); auto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OA : Tpoint, Opp O E E' A OA).
(* Goal: @ex (@Tpoint Tn) (fun OA : @Tpoint Tn => @Opp Tn O E E' A OA) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H A).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H18 OA.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E A).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply not_out_bet in H12;auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Col O E OA).
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Opp in H19.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Sum in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H19.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O OA B OC A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply out_col in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OC O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OC.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O C; Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OA O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OA.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Out Tn O OA E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply not_out_bet in H12.
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
assert(HP:=l5_2 A O E OA H11 H12 H19).
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Out.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
subst OA.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H21.
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
induction HP.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
right; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
left; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; Cong.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' B O D) (@Ps Tn O E D)) *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists B.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' A OA A2 H19 H0).
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' C OC C2 H16 H2).

(****** A<0 ********* B<0 ********** C>0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OB : Tpoint, Opp O E E' B OB).
(* Goal: @ex (@Tpoint Tn) (fun OB : @Tpoint Tn => @Opp Tn O E E' B OB) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H B).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OB.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E B).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H8.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_distinct in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H13.
(* Goal: @Bet Tn B O E *)
(* Goal: @Col Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
bet.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OB).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' B OB); auto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OA : Tpoint, Opp O E E' A OA).
(* Goal: @ex (@Tpoint Tn) (fun OA : @Tpoint Tn => @Opp Tn O E E' A OA) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H A).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H18 OA.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E A).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply not_out_bet in H12;auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Col O E OA).
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Opp in H19.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Sum in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H19.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O OA OB C A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C O D) (@Ps Tn O E D)) *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
exists C.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OA O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OA.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Out Tn O OA E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply not_out_bet in H12.
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
assert(HP:=l5_2 A O E OA H11 H12 H19).
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Out.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
subst OA.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H21.
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
induction HP.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
right; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
left; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
repeat split; Cong;
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OB O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OB.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B; Cong.
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' A OA A2 H19 H0).
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_same_square O E E' B OB B2 H16 H1).


(****** A<0 ********* B<0 ********** C<0 ********)

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OC : Tpoint, Opp O E E' C OC).
(* Goal: @ex (@Tpoint Tn) (fun OC : @Tpoint Tn => @Opp Tn O E E' C OC) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H C).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H15 OC.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E C).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst C.

(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_symmetry in H9.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H9.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_right_comm in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_not_col in H3.
(* Goal: False *)
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply H3.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Bet Tn C O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H14.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OC).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' C OC); auto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OA : Tpoint, Opp O E E' A OA).
(* Goal: @ex (@Tpoint Tn) (fun OA : @Tpoint Tn => @Opp Tn O E E' A OA) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H A).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H18 OA.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E A).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply not_out_bet in H12;auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Col O E OA).
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Opp in H19.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Sum in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Col Tn O E OA *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ar2 in H19.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(exists OB : Tpoint, Opp O E E' B OB).
(* Goal: @ex (@Tpoint Tn) (fun OB : @Tpoint Tn => @Opp Tn O E E' B OB) *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply(opp_exists O E E' H B).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
ex_and H21 OB.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ng O E B).
(* Goal: @Ng Tn O E B *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
unfold Ng.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply cong_identity in H8.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
subst B'.
(* Goal: False *)
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply perp_distinct in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @Bet Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
apply not_out_bet in H13.
(* Goal: @Bet Tn B O E *)
(* Goal: @Col Tn B O E *)
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
bet.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
assert(Ps O E OB).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(opp_neg_pos O E E' B OB); auto.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(pythagoras O E E' A B' O OA OB OC A2 B2 C2); auto.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OC *)
(* Goal: @LeP Tn O E E' O OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply out_col in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OC O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OC.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OC *)
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps in H17.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H16.
(* Goal: @Cong Tn O OC A B' *)
(* Goal: @Length Tn O E E' A O OA *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H16.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O C; Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OA O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OA.
(* Goal: and (@Diff Tn O E E' OA O OA) (@Ps Tn O E OA) *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
split.
(* Goal: @Diff Tn O E E' OA O OA *)
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_diff.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply sum_O_B; Col.
(* Goal: @Ps Tn O E OA *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Ps.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Out Tn O OA E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply not_out_bet in H12.
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
assert(HP:=l5_2 A O E OA H11 H12 H19).
(* Goal: @Out Tn O OA E *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Out.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
subst OA.
(* Goal: False *)
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply cong_identity in H24.
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.
(* Goal: or (@Bet Tn O OA E) (@Bet Tn O E OA) *)
(* Goal: @Col Tn A O E *)
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
induction HP.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
right; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
left; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H19.
(* Goal: @Cong Tn O OA A O *)
(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @Length Tn O E E' B' O OB *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Length.
repeat split; Cong;
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @LeP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LeP.
(* Goal: or (@LtP Tn O E E' O OB) (@eq (@Tpoint Tn) O OB) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
left.
(* Goal: @LtP Tn O E E' O OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' OB O D) (@Ps Tn O E D)) *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
exists OB.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
split; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply diff_A_O; auto.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
Col.
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply opp_midpoint in H22.
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
unfold Midpoint in H22.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B; Cong.
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' A OA A2 H19 H0).
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' B OB B2 H22 H1).
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply(opp_same_square O E E' C OC C2 H16 H2).
Qed.



Lemma PythRel_uniqueness : forall O E E' A B C1 C2,
 PythRel O E E' A B C1 ->
 PythRel O E E' A B C2 ->
 ((Ps O E C1 /\ Ps O E C2) \/ C1 = O)->
 C1 = C2.

Proof.
(* Goal: forall (O E E' A B C1 C2 : @Tpoint Tn) (_ : @PythRel Tn O E E' A B C1) (_ : @PythRel Tn O E E' A B C2) (_ : or (and (@Ps Tn O E C1) (@Ps Tn O E C2)) (@eq (@Tpoint Tn) C1 O)), @eq (@Tpoint Tn) C1 C2 *)
intros.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold PythRel in *.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ar2 in *.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
clean_duplicated_hyps;
(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction H2; induction H3.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.

(* Goal: @Sum Tn O E E' A2 B2 C2 *)
induction H4; induction H3.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst A.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Opp in H3.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply sum_comm in H3; auto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(HP:=sum_pos_pos O E E' C1 C2 O H1 H2 H3).
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(HQ:=O_not_positive O E).
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.


(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Opp in H3.

(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (sum_A_O_eq O E E') in H3; auto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) O A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Opp in H2.
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(HP:=sum_pos_pos O E E' C1 A O H1 H3 H2).
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(HQ:=O_not_positive O E).
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
contradiction.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) O A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Opp in H2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply(sum_O_B_eq O E E') in H2; auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Opp in *.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
eapply (sum_uniquenessA O E E' H A C1 C2 O); auto.


(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ex_and H2 B'.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_distinct in H2.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ex_and H0 B'.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_distinct in H0.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ex_and H0 B1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ex_and H2 B2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Cong O B1 O B2).
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B; Cong.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert (O <> E).
(* Goal: not (@eq (@Tpoint Tn) O E) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst E.
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply H;Col.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(HH:= perp2__col O B1 B2 O B H0 H2).

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(B1 = B2 \/ Midpoint O B1 B2).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply l7_20; Col.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H13.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
clean_duplicated_hyps.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
clean_trivial_hyps.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Cong O C2 O C1).
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with A B1; Cong.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(C1 = C2 \/ Midpoint O C1 C2).
(* Goal: or (@eq (@Tpoint Tn) C1 C2) (@Midpoint Tn O C1 C2) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l7_20.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H5.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H1.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Out O C1 C2).
apply (out2_out_1 _ _ _ E);
apply l6_6;
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Midpoint in H5.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l6_4_1 in H5; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Midpoint in H5.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_symmetry in H5.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (cong_identity O C2 O);auto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction(eq_dec_points A O).
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst A.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Cong O C1 O C2).
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B2; trivial.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with O B1; Cong.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(C1 = C2 \/ Midpoint O C1 C2).
(* Goal: @Col Tn O E OB *)
(* Goal: @Cong Tn O OB B' O *)
(* Goal: @Prod Tn O E E' OA OA A2 *)
(* Goal: @Prod Tn O E E' OB OB B2 *)
(* Goal: @Prod Tn O E E' OC OC C2 *)
apply l7_20; eCol.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H15.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H1.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H2.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Out O C1 C2).
apply (out2_out_1 _ _ _ E);
apply l6_6;
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Midpoint in H15.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l6_4_1 in H15; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_symmetry in H5.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (cong_identity O C2 O);auto.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Per A O B1).
(* Goal: @Per Tn A O B1 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_in_per.
(* Goal: @Perp_at Tn O A O O B1 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn O O A B1 O *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply perp_perp_in.

(* Goal: @Perp Tn O A B1 O *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (perp_col O B ).
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Perp.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Per in H15.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ex_and H15 B2'.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(B2 = B2').
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (symmetric_point_uniqueness B1 O); auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst B2'.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Cong O C1 O C2).
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with A B2; trivial.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply cong_transitivity with A B1; Cong.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(C1 = C2 \/ Midpoint O C1 C2).
(* Goal: or (@eq (@Tpoint Tn) C1 C2) (@Midpoint Tn O C1 C2) *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l7_20.
(* Goal: @Col Tn C1 O C2 *)
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
ColR.
(* Goal: @Cong Tn O C1 O C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
Cong.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H18.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assumption.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
induction H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H1.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Ps in H19.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
assert(Out O C1 C2).
apply (out2_out_1 _ _ _ E);
apply l6_6;
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
auto.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
unfold Midpoint in H18.
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply l6_4_1 in H18; auto.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
tauto.

(* Goal: @eq (@Tpoint Tn) C1 C2 *)
subst C1.
(* Goal: @eq (@Tpoint Tn) O C2 *)
apply cong_symmetry in H17.
(* Goal: not (@eq (@Tpoint Tn) O A) *)
(* Goal: @Perp Tn O B B1 O *)
(* Goal: @Col Tn O B A *)
(* Goal: @eq (@Tpoint Tn) C1 C2 *)
apply (cong_identity O C2 O);auto.
Qed.



End PythagoreanFun.



