(***************************************************************************)
(* Formalization of the Chou, Gao and Zhang's decision procedure.          *)
(* Julien Narboux (Julien@narboux.fr)                                      *)
(* LIX/INRIA FUTURS 2004-2006                                              *)
(* University of Strasbourg 2008-2009                                      *)
(***************************************************************************)

Require Export euclidean_constructions.
Require Export area_elimination_lemmas.
Require Export ratios_elimination_lemmas.

(* lemme 3_2 chou *)
Lemma l_24_a : forall A B P D,
Col A D B -> perp A B P D ->
A<>B -> B<>D ->
 A**D / D**B = Py P A B / Py P B A.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: False *)
unfold perp, Py4, Py in *.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg A D) (Fopp (DSeg B D))) (Fdiv (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg B P) (DSeg B P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg A P) (DSeg A P)))) *)
IsoleVar (A ** P * A ** P) H0.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
rewrite H0.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg A D) (Fopp (DSeg B D))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg B P) (DSeg B P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A B) (DSeg A B))) (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))))) *)
assert (A**D+D**B = A**B).
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
(* Goal: @eq F (Fdiv (DSeg A D) (Fopp (DSeg B D))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg B P) (DSeg B P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A B) (DSeg A B))) (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))))) *)
eapply chasles;auto.
(* Goal: @eq F (Fdiv (DSeg A D) (Fopp (DSeg B D))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg B P) (DSeg B P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A B) (DSeg A B))) (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))))) *)
assert (A**B * A**B = A**D * A**D + B**D* B**D + 2 * A**D*D**B).
(* Goal: @eq F (DSeg O B) (DSeg O C) *)
(* Goal: @eq Point B C *)
rewrite <- H3.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg A P) (DSeg A P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A P) (DSeg A P))) (Fmult (DSeg A B) (DSeg A B)))) F0 *)
(* Goal: False *)
rewrite H4.
cut (B ** P * B ** P + P ** D * P ** D - B ** D * B ** D + A ** D * A ** D -
 P ** D * P ** D +
 (A ** D * A ** D + B ** D * B ** D + 2 * A ** D * - B ** D) -
 B ** P * B ** P = 2* A**D * A**B).
(* Goal: forall _ : @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))), @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
intro Ha.
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Ha.
cut ((B ** P * B ** P +
 (A ** D * A ** D + B ** D * B ** D + 2 * A ** D * - B ** D) -
 (B ** P * B ** P + P ** D * P ** D - B ** D * B ** D + A ** D * A ** D -
  P ** D * P ** D) = 2 * D**B * A**B)).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
(* Goal: @eq F (Fdiv (Fmult (Fdiv (DSeg Q S) (DSeg B D)) (Py4 P B R D)) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Hb.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fdiv (DSeg A D) (Fopp (DSeg B D))) (Fdiv (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg B D))) (DSeg A B))) *)
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fplus (Fplus (Fmult (DSeg A D) (DSeg A D)) (Fmult (DSeg B D) (DSeg B D))) (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (Fopp (DSeg B D))))) (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D)))) (Fmult (Fmult (Fplus F1 F1) (DSeg D B)) (DSeg A B)) *)
(* Goal: @eq F (Fminus (Fplus (Fminus (Fplus (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg P D) (DSeg P D))) (Fmult (DSeg B D) (DSeg B D))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg P D) (DSeg P D))) (Fplus (Fplus (Fmult (DSeg A D) (DSeg A D)) (Fmult (DSeg B D) (DSeg B D))) (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (Fopp (DSeg B D))))) (Fmult (DSeg B P) (DSeg B P))) (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A B)) *)
field;repeat split;auto with Geom.
(* Goal: @eq F (DSeg O B) (DSeg O C) *)
(* Goal: @eq Point B C *)
rewrite <- H3.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: @eq F (DSeg O B) (DSeg O C) *)
(* Goal: @eq Point B C *)
rewrite <- H3.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
Qed.

Lemma perp4_perp : forall A B P, 
perp A B P A -> Py P A B = 0.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py P A B) F0 *)
unfold perp in H.
(* Goal: @eq F (Py P A B) F0 *)
rewrite py4_simpl_6 in H.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
assumption.
Qed.

Lemma perp_not_eq_not_perp : forall A B P D, perp A B P D ->
Col A D B ->
 A <> B ->  B <> D -> A <> D -> 
Py P A B <> 0.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (Py P A B) F0) *)
unfold not;intro.
(* Goal: False *)
assert (perp A B P A).
(* Goal: not (perp C D C D) *)
unfold perp, Py4.
(* Goal: @eq Point A B *)
(* Goal: False *)
unfold Py in *.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg A P) (DSeg A P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A P) (DSeg A P))) (Fmult (DSeg A B) (DSeg A B)))) F0 *)
(* Goal: False *)
IsoleVar (A ** B * A ** B) H4.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg A P) (DSeg A P))) (Fminus (Fplus (Fmult (DSeg B P) (DSeg B P)) (Fmult (DSeg A P) (DSeg A P))) (Fmult (DSeg A B) (DSeg A B)))) F0 *)
(* Goal: False *)
rewrite H4.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: False *)
unfold perp, Py4, Py in *.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: False *)
IsoleVar (B ** P * B ** P) H4.
(* Goal: False *)
rewrite H4 in H.
(* Goal: False *)
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
ring_simplify in H.
(* Goal: False *)
replace (A ** B) with (A**D + D**B) in H.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: False *)
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
ring_simplify in H.
replace (- (2) * A ** D * A ** D + 2 * A ** D * B ** D ) with 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
(2* A**D * (B**D - A**D)) in H by ring.
(* Goal: False *)
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
assert ((2* A**D * B**A) <> 0).
(* Goal: not (@eq F (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) F0) *)
(* Goal: @eq F (Py A B A) (Fplus (Py P A B) (Py P B A)) *)
repeat (apply nonzeromult);auto with Geom.
(* Goal: False *)
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
replace (B ** D - A ** D) with (B**D + D**A) in H.
(* Goal: False *)
(* Goal: @eq F (Fplus (DSeg B D) (DSeg D A)) (Fminus (DSeg B D) (DSeg A D)) *)
(* Goal: @eq F (Fplus (DSeg A D) (DSeg D B)) (DSeg A B) *)
replace (B ** D + D ** A) with (B**A) in H.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
symmetry;
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
uniformize_dir_seg;ring.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

(* lemma 3_2 chou *)
Lemma l_24_b : forall A B P D,
Col A D B -> perp A B P D ->
A<>B -> 
 A**D / A**B = Py P A B / (2 * A**B * A**B).
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
cases_equality B D.
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
subst D.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field_simplify_eq; auto with Geom.
(* Goal: @eq F (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg P A) (DSeg P A))) (Fmult (DSeg P B) (DSeg P B))) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
unfold perp, Py4, Py in H0.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (Fopp (DSeg A P)) (Fopp (DSeg A P)))) (Fmult (Fopp (DSeg B P)) (Fopp (DSeg B P)))) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
IsoleVar (A ** B * A ** B) H0.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (2 * A ** B * A ** B) with (2* (A ** B * A ** B)) by ring.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
rewrite H0.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
cases_equality A D.
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
subst D.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv F0 (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
rewrite perp4_perp by auto.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
split;auto with Geom.
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
assert (Py P A B <> 0).

(* Goal: not (@eq F (Py P A B) F0) *)
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
eapply perp_not_eq_not_perp;eauto.
(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
assert (Py P B A <> 0).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_not_eq_not_perp B A P D);auto with Geom.

(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
replace (A**D / A**B) with (1/ (A**B / A**D)) by (field;auto with Geom).
(* Goal: @eq F (Fdiv F1 (Fdiv (DSeg A B) (DSeg A D))) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
replace (2 * A ** B * A ** B) with (Py A B A) by (unfold Py;uniformize_dir_seg;basic_simpl;ring).
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (A**B) with (A**D + D**B) by auto with Geom.
(* Goal: @eq F (Fdiv F1 (Fdiv (Fplus (DSeg A D) (DSeg D B)) (DSeg A D))) (Fdiv (Py P A B) (Py A B A)) *)
replace ((A ** D + D ** B) / A ** D) with (1 + D ** B / A ** D) by (field;auto with Geom).
(* Goal: @eq F (Fdiv F1 (Fplus F1 (Fdiv (DSeg D B) (DSeg A D)))) (Fdiv (Py P A B) (Py A B A)) *)
replace (D ** B / A ** D) with (1/ (A**D / D**B)) by (field; auto with Geom).
(* Goal: @eq F (Fdiv F1 (Fplus F1 (Fdiv F1 (Fdiv (DSeg A D) (DSeg D B))))) (Fdiv (Py P A B) (Py A B A)) *)
rewrite (l_24_a A B P D) by auto.
(* Goal: @eq F (Fdiv F1 (Fplus F1 (Fdiv F1 (Fdiv (Py P A B) (Py P B A))))) (Fdiv (Py P A B) (Py A B A)) *)
replace (1 / (1 + 1 / (Py P A B / Py P B A))) with ((Py P A B / (Py P A B + Py P B A))).
(* Goal: not (@eq F (Fplus (Py P A B) (Py P B A)) F0) *)
replace (Py P A B + Py P B A) with (Py A B A).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
unfold Py;basic_simpl;uniformize_dir_seg;ring.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto.
(* Goal: not (@eq F (Fplus (Py P A B) (Py P B A)) F0) *)
replace (Py P A B + Py P B A) with (Py A B A).
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (A ** B * A ** B + A ** B * A ** B) with (2*  A ** B * A ** B) by ring.
(* Goal: not (@eq F (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) F0) *)
(* Goal: @eq F (Py A B A) (Fplus (Py P A B) (Py P B A)) *)
repeat (apply nonzeromult);auto with Geom.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
unfold Py;basic_simpl;uniformize_dir_seg;ring.
Qed.

(* lemma 3_2 chou *)
Lemma l_24_c : forall A B P D,
Col A D B -> perp A B P D ->
A<>B -> 
 D**B / A**B = Py P B A / (2 * A**B * A**B).
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg D B) (DSeg A B)) (Fdiv (Py P B A) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
assert (B ** D / B ** A = Py P B A / (2 * B ** A * B ** A)).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply l_24_b ;auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (D ** B / A ** B) with (B ** D / B ** A) by auto with Geom.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Fdiv (Py P B A) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B A))) (Fdiv (Py P B A) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
replace (2*B ** A * B ** A) with (2*A ** B * A ** B) .
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
uniformize_dir_seg;ring.
Qed.

Lemma l_24_c_on_foot : forall P U V Y,
on_foot Y P U V ->
U**Y / U**V = Py P U V / Py U V U.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: per A F B *)
unfold on_foot in H.
(* Goal: per A F B *)
use H.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (U ** Y / U ** V) with (Y**U/ V**U) by auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite (l_24_c V U P) by auto with Geom.
(* Goal: @eq F (Fdiv (Py P U V) (Fmult (Fmult (Fplus F1 F1) (DSeg V U)) (DSeg V U))) (Fdiv (Py P U V) (Py U V U)) *)
replace (2 * V ** U * V ** U) with (Py U V U).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
unfold Py;basic_simpl;uniformize_dir_seg;ring.
Qed.

Lemma per_area: forall A B C,
  per A B C -> 
  2 * 2 * S A B C * S A B C = A**B * A**B * B**C * B**C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (DSeg B C) F0) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality B C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A B) (DSeg A B)) (DSeg B C)) (DSeg B C)) *)
assert (on_foot B A B C).
(* Goal: on_foot B A B C *)
(* Goal: @eq F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A B) (DSeg A B)) (DSeg B C)) (DSeg B C)) *)
unfold on_foot.
(* Goal: and (perp B A B C) (and (Col B B C) (not (@eq Point B C))) *)
(* Goal: @eq F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A B) (DSeg A B)) (DSeg B C)) (DSeg B C)) *)
repeat split.
(* Goal: perp B A B C *)
(* Goal: Col B B C *)
(* Goal: not (@eq Point B C) *)
(* Goal: @eq F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A B) (DSeg A B)) (DSeg B C)) (DSeg B C)) *)
cut (perp B C B A).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (perp C D C D) *)
unfold perp, Py4.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py C B A) with (Py A B C) by auto with Geom.
(* Goal: @eq F (Fplus (Fmult (Fplus F1 F1) (Py A O A)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A B) (DSeg A B)) (DSeg B C)) (DSeg B C)) *)
apply on_foot_area.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.

Lemma per_col_eq : forall A B C,
 per A B C -> Col A B C -> A = B \/ B = C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
unfold per in H.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
rewrite col_pyth in H by assumption.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
cases_equality A B.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
left;auto.
right.
IsoleVar (B**C) H.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:solve_conds;auto with Geom.
replace (0 / (2 * B ** A)) with 0 in H 
  by (field;solve_conds;auto with Geom).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma perp_col_perp : forall P Q B C,
 Q<>B ->
 per P Q B -> Col Q B C -> per P Q C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: per P Q C *)
cut (perp P Q Q C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (perp P Q Q B) by auto with Geom.
(* Goal: perp P Q Q C *)
cut (perp Q C P Q).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_para_perp  Q B P Q Q C);auto with Geom.
Qed.

Lemma l_3_4 : forall A B C P,
 Col A B C -> Py P A C <> 0 ->
 Py P A B / Py P A C = A**B/ A**C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
cases_equality A B.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg B C) F0) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality B C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
basic_simpl;auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
assert (A<>C).
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
basic_simpl;intuition.

(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
elim (proj_ex P A B H1).
(* Goal: forall (x : Point) (_ : on_foot x P A B), @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
intros Q HQ.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
unfold on_foot in *.
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
use HQ.

(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality A Q.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fdiv (Py P Q B) (Py P Q C)) (Fdiv (DSeg Q B) (DSeg Q C)) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
clear H5.
(* Goal: @eq F (Fdiv (Py P Q B) (Py P Q C)) (Fdiv (DSeg Q B) (DSeg Q C)) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
unfold perp, Py4 in H3.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Py P Q B) (Py P Q C)) (Fdiv (DSeg Q B) (DSeg Q C)) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
IsoleVar (Py P Q B) H3.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.


(* Goal: @eq F (Fdiv (Py P Q B) (Py P Q C)) (Fdiv (DSeg Q B) (DSeg Q C)) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
assert (T:=perp_col_perp P Q B C H6 H3 H).
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.

(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
assert (perp A C Q P).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_para_perp A B Q P A C);auto with Geom.
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
unfold parallel.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (perp Q P A C)by auto with Geom.
(* Goal: not (perp A B A B) *)
unfold perp, Py4 in *.
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
IsoleVar (Py P A B) H3.
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
IsoleVar (Py P A C) H8.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
(* Goal: @eq F (Fdiv (Py Q A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
rewrite H8.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
rewrite (col_pyth Q A B) by assumption.
(* Goal: @eq F (Fdiv (Fmult (Fmult (Fplus F1 F1) (DSeg A Q)) (DSeg A B)) (Py Q A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
rewrite (col_pyth Q A C).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto with Geom.
(* Goal: Col Q A C *)
assert (Col A Q C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply  (col_trans_1 A B Q C H1); auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Require Export Classical.

Lemma per_dec : forall A B C,
 per A B C \/ ~ per A B C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
elim (classic (Py A B C = 0));
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
Qed.

(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
Ltac cases_per A B C := elim (per_dec A B C);intros.

Lemma l_3_4_b : forall A B C P,
 Col A B C ->
 Py P A B * A**C =  Py P A C * A**B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
cases_per P A C.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
unfold per in H0.

(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
rewrite H0.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult F0 (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
cases_equality A C.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
subst;basic_simpl;auto.
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult F0 (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
assert (Py P A B = 0).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_col_perp P A C B H1);auto with Geom.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
basic_simpl;auto.

(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
assert (T:=l_3_4 A B C P H H0).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
IsoleVar (Py P A B) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
(* Goal: not (@eq F (Py P A C) F0) *)
assert (A=C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.

Lemma l_28_b : forall A B U V Y,
U <> V ->
Col Y U V -> 
Py A B Y = U**Y/U**V * Py A B V + Y**V/U**V * Py A B U.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (Py A V B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (Py A U B))) (Fmult (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (Fdiv (DSeg Y V) (DSeg U V))) (Py U V U))) *)
set (r1 := U ** Y / U ** V).
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (Py A U B))) (Fmult (Fmult r1 (Fdiv (DSeg Y V) (DSeg U V))) (Py U V U))) *)
set (r2 := Y ** V / U ** V).
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
assert (r2 = 1 -r1).
(* Goal: @eq F r2 (Fminus F1 r1) *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   unfold r1, r2.
(* Goal: @eq F (Fdiv (DSeg Y V) (DSeg U V)) (Fminus F1 (Fdiv (DSeg U Y) (DSeg U V))) *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   rewrite <- (chasles Y U V).
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
   uniformize_dir_seg.
(* Goal: not (@eq F (DSeg P Q) F0) *)
   field;auto with Geom.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   assumption.

(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
cut (B**Y * B**Y = r2 * U**B * U**B + r1 * V**B * V**B - r1 * r2 * U**V * U**V).
(* Goal: forall _ : @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))), @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
intro Ha.
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
cut (A**Y * A**Y = r2 * U**A * U**A + r1 * V**A * V**A - r1 * r2 * U**V * U**V).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Ha.
(* Goal: @eq F (Fdiv (Fmult (Fdiv (DSeg Q S) (DSeg B D)) (Py4 P B R D)) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Hb.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg B U)) (DSeg B U)) (Fmult (Fmult r1 (DSeg B V)) (DSeg B V))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V)))) (Fminus (Fplus (Fmult (Fmult r2 (DSeg A U)) (DSeg A U)) (Fmult (Fmult r1 (DSeg A V)) (DSeg A V))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V)))) (Fplus (Fmult r1 (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B V) (DSeg B V))) (Fmult (DSeg A V) (DSeg A V)))) (Fmult r2 (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B U) (DSeg B U))) (Fmult (DSeg A U) (DSeg A U))))) *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
assert ( (A ** B * A ** B) = (r1 + r2) * (A ** B * A ** B)) by (rewrite H1;ring).
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg B U)) (DSeg B U)) (Fmult (Fmult r1 (DSeg B V)) (DSeg B V))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V)))) (Fminus (Fplus (Fmult (Fmult r2 (DSeg A U)) (DSeg A U)) (Fmult (Fmult r1 (DSeg A V)) (DSeg A V))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V)))) (Fplus (Fmult r1 (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B V) (DSeg B V))) (Fmult (DSeg A V) (DSeg A V)))) (Fmult r2 (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B U) (DSeg B U))) (Fmult (DSeg A U) (DSeg A U))))) *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
rewrite H2 at 1.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.

(* first cut *)
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
replace ((1 - r1) * U ** A * U ** A + r1 * V ** A * V ** A -
r1 * (1 - r1) * U ** V * U ** V)
with (U ** A * U ** A + r1 * (V ** A * V ** A - U ** A * U ** A - U ** V * U ** V) 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
      + r1 *r1 *  U ** V * U ** V) by ring.
replace (U ** A * U ** A + r1 * (V ** A * V ** A - U ** A * U ** A - U ** V * U ** V) +
r1 * r1 * U ** V * U ** V) with
(U ** A * U ** A + r1 * r1 * U**V * U**V - r1 * Py A U V)
by (unfold Py; uniformize_dir_seg; ring).

(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (DSeg U A) (DSeg U A)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py A U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
cut (r1 * Py A U V = Py A U Y).
(* Goal: forall _ : @eq F (Fmult r1 (Py B U V)) (Py B U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hab.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rewrite Hab.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
cut (r1 * U**V = U**Y).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
assert (r1 * r1 * U ** V * U ** V = U**Y * U**Y)
by (rewrite <- Hb;ring).

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.

(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
assert (Py A U V * U ** Y = Py A U Y * U ** V).
(* Goal: @eq F (Fmult (Py A U V) (DSeg U Y)) (Fmult (Py A U Y) (DSeg U V)) *)
(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
apply (l_3_4_b U V Y A).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rename H2 into T.
(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
IsoleVar (Py A U Y) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* second cut *)
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
replace ((1 - r1) * U ** B * U ** B + r1 * V ** B * V ** B -
r1 * (1 - r1) * U ** V * U ** V)
with (U ** B * U ** B + r1 * (V ** B * V ** B - U ** B * U ** B - U ** V * U ** V) 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
      + r1 *r1 *  U ** V * U ** V) by ring.
replace (U ** B * U ** B + r1 * (V ** B * V ** B - U ** B * U ** B - U ** V * U ** V) +
r1 * r1 * U ** V * U ** V) with
(U ** B * U ** B + r1 * r1 * U**V * U**V - r1 * Py B U V)
by (unfold Py; uniformize_dir_seg; ring).

(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
cut (r1 * Py B U V = Py B U Y).
(* Goal: forall _ : @eq F (Fmult r1 (Py B U V)) (Py B U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hab.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rewrite Hab.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
cut (r1 * U**V = U**Y).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
assert (r1 * r1 * U ** V * U ** V = U**Y * U**Y)
by (rewrite <- Hb;ring).

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
assert (Py B U V * U ** Y = Py B U Y * U ** V).
(* Goal: @eq F (Fmult (Py B U V) (DSeg U Y)) (Fmult (Py B U Y) (DSeg U V)) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
apply (l_3_4_b U V Y B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rename H2 into T.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
IsoleVar (Py B U Y) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma l3_5_py : forall A B U V Y,
  U <> V ->
  Col Y U V ->  
  Py A Y B = U**Y / U**V * Py A V B + Y**V/ U**V * Py A U B 
  - (U**Y/ U**V) * (Y**V / U**V) * Py U V U.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (Py A V B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (Py A U B))) (Fmult (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (Fdiv (DSeg Y V) (DSeg U V))) (Py U V U))) *)
set (r1 := U ** Y / U ** V).
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (Py A U B))) (Fmult (Fmult r1 (Fdiv (DSeg Y V) (DSeg U V))) (Py U V U))) *)
set (r2 := Y ** V / U ** V).
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
assert (r2 = 1 -r1).
(* Goal: @eq F r2 (Fminus F1 r1) *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   unfold r1, r2.
(* Goal: @eq F (Fdiv (DSeg Y V) (DSeg U V)) (Fminus F1 (Fdiv (DSeg U Y) (DSeg U V))) *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   rewrite <- (chasles Y U V).
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
   uniformize_dir_seg.
(* Goal: not (@eq F (DSeg P Q) F0) *)
   field;auto with Geom.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
   assumption.

(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
cut (B**Y * B**Y = r2 * U**B * U**B + r1 * V**B * V**B - r1 * r2 * U**V * U**V).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
cut (A**Y * A**Y = r2 * U**A * U**A + r1 * V**A * V**A - r1 * r2 * U**V * U**V).
(* Goal: forall _ : @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))), @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U A)) (DSeg U A)) (Fmult (Fmult r1 (DSeg V A)) (DSeg V A))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
intro Ha.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Ha.
replace (Y ** B * Y ** B) with (B ** Y * B ** Y)
  by (uniformize_dir_seg;field).
(* Goal: @eq F (Fdiv (Fmult (Fdiv (DSeg Q S) (DSeg B D)) (Py4 P B R D)) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Hb.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
replace ((1 - r1) * U ** A * U ** A + r1 * V ** A * V ** A -
r1 * (1 - r1) * U ** V * U ** V)
with (U ** A * U ** A + r1 * (V ** A * V ** A - U ** A * U ** A - U ** V * U ** V) 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
      + r1 *r1 *  U ** V * U ** V) by ring.
replace (U ** A * U ** A + r1 * (V ** A * V ** A - U ** A * U ** A - U ** V * U ** V) +
r1 * r1 * U ** V * U ** V) with
(U ** A * U ** A + r1 * r1 * U**V * U**V - r1 * Py A U V)
by (unfold Py; uniformize_dir_seg; ring).

(* first cut *)
(* Goal: @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (DSeg U A) (DSeg U A)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py A U V))) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
cut (r1 * Py A U V = Py A U Y).
(* Goal: forall _ : @eq F (Fmult r1 (Py B U V)) (Py B U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hab.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rewrite Hab.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
cut (r1 * U**V = U**Y).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg A Y) (DSeg A Y)) (Fminus (Fplus (Fmult (DSeg A U) (DSeg A U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg A U) (DSeg A U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg A Y) (DSeg A Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
intro Hbb.
assert (r1 * r1 * U ** V * U ** V = U**Y * U**Y)
by (rewrite <- Hbb;ring).

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.

(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
assert (Py A U V * U ** Y = Py A U Y * U ** V).
(* Goal: @eq F (Fmult (Py A U V) (DSeg U Y)) (Fmult (Py A U Y) (DSeg U V)) *)
(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
apply (l_3_4_b U V Y A).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rename H2 into T.
(* Goal: @eq F (Fmult r1 (Py A U V)) (Py A U Y) *)
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (Fmult r2 (DSeg U B)) (DSeg U B)) (Fmult (Fmult r1 (DSeg V B)) (DSeg V B))) (Fmult (Fmult (Fmult r1 r2) (DSeg U V)) (DSeg U V))) *)
IsoleVar (Py A U Y) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* second cut *)
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
replace ((1 - r1) * U ** B * U ** B + r1 * V ** B * V ** B -
r1 * (1 - r1) * U ** V * U ** V)
with (U ** B * U ** B + r1 * (V ** B * V ** B - U ** B * U ** B - U ** V * U ** V) 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
      + r1 *r1 *  U ** V * U ** V) by ring.
replace (U ** B * U ** B + r1 * (V ** B * V ** B - U ** B * U ** B - U ** V * U ** V) +
r1 * r1 * U ** V * U ** V) with
(U ** B * U ** B + r1 * r1 * U**V * U**V - r1 * Py B U V)
by (unfold Py; uniformize_dir_seg; ring).

(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
cut (r1 * Py B U V = Py B U Y).
(* Goal: forall _ : @eq F (Fmult r1 (Py B U V)) (Py B U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hab.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg U B) (DSeg U B)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fmult r1 (Py B U V))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rewrite Hab.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
cut (r1 * U**V = U**Y).
(* Goal: forall _ : @eq F (Fmult r1 (DSeg U V)) (DSeg U Y), @eq F (Fmult (DSeg B Y) (DSeg B Y)) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (Fmult (Fmult r1 r1) (DSeg U V)) (DSeg U V))) (Fminus (Fplus (Fmult (DSeg B U) (DSeg B U)) (Fmult (DSeg U Y) (DSeg U Y))) (Fmult (DSeg B Y) (DSeg B Y)))) *)
(* Goal: @eq F (Fmult r1 (DSeg U V)) (DSeg U Y) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
intro Hb.
assert (r1 * r1 * U ** V * U ** V = U**Y * U**Y)
by (rewrite <- Hb;ring).

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
assert (Py B U V * U ** Y = Py B U Y * U ** V).
(* Goal: @eq F (Fmult (Py B U V) (DSeg U Y)) (Fmult (Py B U Y) (DSeg U V)) *)
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
apply (l_3_4_b U V Y B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
rename H2 into T.
(* Goal: @eq F (Fmult r1 (Py B U V)) (Py B U Y) *)
IsoleVar (Py B U Y) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold r1;field; auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma midpoint_ratio_1 : forall O B D,
mid_point O B D ->  B<>D -> B ** O / B ** D = 1/2.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: per A F B *)
use H.
(* Goal: @eq F (Fdiv (DSeg B O) (DSeg B D)) (Fdiv F1 (Fplus F1 F1)) *)
assert (B**D = B**O + O**D).
(* Goal: not (@eq F (DSeg P Q) F0) *)
symmetry;auto with Geom.
(* Goal: @eq F (Fplus (Fmult (Fplus F1 F1) (Py A O A)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
split;auto with Geom.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (O ** D + O ** D) with (2*O**D) by ring.
(* Goal: not (@eq F (Fmult (Py Q A B) (DSeg P Q)) F0) *)
apply nonzeromult.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (O=D);auto with Geom.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fplus (Py P B Q) (Py P B Q)) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst O.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (B=D); auto with Geom.
Qed.

Lemma midpoint_ratio_2 : forall O B D,
mid_point O B D ->  B<>D -> O ** D / B ** D = 1/2.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: per A F B *)
use H.
(* Goal: @eq F (DSeg O B) (Fopp (DSeg O D)) *)
(* Goal: @eq Point B C *)
rewrite <- H2.
(* Goal: @eq F (Fdiv (DSeg B O) (DSeg B D)) (Fdiv F1 (Fplus F1 F1)) *)
apply midpoint_ratio_1.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold mid_point;auto.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.

Lemma l_28_midpoint : forall O A B P Q,
 mid_point O A B ->
 2 * Py O P Q = Py A P Q + Py B P Q.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
cases_equality A B.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst A.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py O P Q)) (Fplus (Py B P Q) (Py B P Q)) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py O P Q)) (Fplus (Py A P Q) (Py B P Q)) *)
assert (O=B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fplus (Py P B Q) (Py P B Q)) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst O.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: @eq F (Fmult (Fplus F1 F1) (Py O P Q)) (Fplus (Py A P Q) (Py B P Q)) *)
assert (Col O A B).
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: not (@eq F (DSeg P Q) F0) *)
use H;auto with Geom.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py O P Q)) (Fplus (Py A P Q) (Py B P Q)) *)
assert (T:=l_28_b Q P A B O H0 H1).
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py O P Q) with (Py Q P O) by auto with Geom.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (Fminus (Py A C D) (Py B C D)) (Fminus F0 (Py D C D))) (Fdiv (Fminus (Py A C D) (Py B C D)) (Fopp (Py C D C))) *)
(* Goal: not (perp C D C D) *)
uniformize_pys.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg A O) (DSeg A B)) (Py B P Q)) (Fmult (Fdiv (DSeg O B) (DSeg A B)) (Py A P Q)))) (Fplus (Py A P Q) (Py B P Q)) *)
replace (A ** O / A ** B) with (1/2).
(* Goal: @eq F (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B P Q)) (Fmult (Fdiv (DSeg O B) (DSeg A B)) (Py A P Q)))) (Fplus (Py A P Q) (Py B P Q)) *)
(* Goal: @eq F (Fdiv F1 (Fplus F1 F1)) (Fdiv (DSeg A O) (DSeg A B)) *)
replace (O ** B / A ** B) with (1/2).
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
(* Goal: @eq Point B C *)
symmetry.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (midpoint_ratio_2);auto.
(* Goal: @eq Point B C *)
symmetry.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (midpoint_ratio_1);auto.
Qed.

Lemma l_28_b_midpoint : forall O A B P Q,
 mid_point O A B ->
 2 * Py P O Q = Py P A Q + Py P B Q - 1/ 2 * Py A B A.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
cases_equality A B.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst A.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (O=B) by auto with Geom.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fplus (Py P B Q) (Py P B Q)) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst O.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
rewrite ( l3_5_py P Q A B O) by
 (unfold mid_point in *;intuition;auto with Geom).
replace (A ** O / A ** B) with (1/2)
 by (symmetry;apply (midpoint_ratio_1);auto).
replace (O ** B / A ** B) with (1/2)
 by (symmetry;apply (midpoint_ratio_2);auto).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma l_27_a : forall A B C D P Q, weak_3_parallelogram A B C D ->
Py A P Q + Py C P Q = Py B P Q + Py D P Q.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
elim H; intros O HO; clear H.
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
use HO.
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
assert (T:= l_28_midpoint O A C P Q H).
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
assert (U:= l_28_midpoint O B D P Q H0).
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
congruence.
Qed.

Lemma l_27_b : forall A B C D P Q, weak_3_parallelogram A B C D ->
Py4 A P B Q = Py4 D P C Q.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.
(* Goal: @eq F (Fminus (Py A P Q) (Py B P Q)) (Fminus (Py D P Q) (Py C P Q)) *)
apply (l_27_a A B C D P Q) in H.
(* Goal: @eq F (Fminus (Py A P Q) (Py B P Q)) (Fminus (Py D P Q) (Py C P Q)) *)
IsoleVar (Py A P Q) H.
(* Goal: @eq F (Fplus (Fmult (Fplus F1 F1) (Py A O A)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
Qed.

Lemma midpoint_is_midpoint: forall I A B, 
 mid_point I A B -> A<>B -> is_midpoint I A B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
assert (A ** I / A ** B = 1 / 2) by
(apply (midpoint_ratio_1 I A B);auto).
(* Goal: is_midpoint I A B *)
unfold is_midpoint, on_line_d, mid_point in *.
(* Goal: per A F B *)
use H.
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto with Geom.
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
IsoleVar (A**I) H1.
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma midpoint_on_line_d: forall I A B, 
 mid_point I A B -> A<>B -> on_line_d A I B (0-1).
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: on_line_d A I B (Fminus F0 F1) *)
unfold on_line_d.
(* Goal: per A F B *)
use H.
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto with Geom.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (A=B);auto with Geom.
(* Goal: @eq F (DSeg O B) (Fopp (DSeg O D)) *)
(* Goal: @eq Point B C *)
rewrite <- H2.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
Qed.

Lemma symmetric_point_unicity : forall O B C D, 
 mid_point O B D ->
 mid_point O D C ->
 B=C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: per A F B *)
use H.
(* Goal: @eq Point B C *)
use H0.
(* Goal: @eq Point B C *)
cases_equality D O.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
 subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
 basic_simpl.
(* Goal: @eq Point B C *)
(* Goal: @eq Point B C *)
 assert (O=C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
 auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
 subst.
(* Goal: not (@eq F (DSeg P Q) F0) *)
 auto with Geom.
assert (Col O B C) by
(apply (col_trans_1 O D B C);auto with Geom).
(* Goal: @eq Point B C *)
assert (O**B=O**C).
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (DSeg O B) (DSeg O C) *)
(* Goal: @eq Point B C *)
rewrite <- H3.
(* Goal: @eq F (DSeg O B) (Fopp (DSeg O D)) *)
(* Goal: @eq Point B C *)
rewrite <- H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: @eq Point B C *)
cases_equality O B.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq Point B C *)
symmetry.
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (A2b O B C B 1);auto with Geom.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.


Lemma weak_3_parallelogram_parallel : forall A B C D,
   weak_3_parallelogram A B C D -> parallel B C A D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
elim H;intros O HO;use HO;clear H.

(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
cases_equality A D.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: not (@eq F (DSeg B C) F0) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality B C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult F0 (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
cases_equality A C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq Point B C *)
(* Goal: @eq Point B C *)
assert (O=C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
use H1.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
cases_equality B D.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
assert (O=D).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: @eq Point B C *)
use H0.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

apply (midpoint_is_midpoint) in H0.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
apply (midpoint_on_line_d) in H1.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
unfold is_midpoint in *.


(* Goal: parallel Y B P1 P *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
unfold parallel, S4.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (S B A C) with (S A C B) by auto with Geom.
rewrite (elim_area_on_line_d A C O D B (0-1)).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (S B C D) with (S C D B) by auto with Geom.
rewrite (elim_area_on_line_d C D O D B (0-1)).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
clear H1.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fminus (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) (Fmult (DSeg B D) (DSeg B D)))) (Fopp (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
ring_simplify_eq.
unfold is_midpoint in *.
rewrite (elim_area_on_line_d A C A C O (1/2)) .
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
rewrite (elim_area_on_line_d C D A C O (1/2)) .
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S V A B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S U A B))) (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S A B V)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S A B U))) *)
uniformize_signed_areas.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
Qed.

Lemma eq_half_eq_zero : forall x : F, x = 1/2 * x -> x=0.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
assert (x-1/2 * x=0).
rewrite H at 1.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
replace (x-1/2*x) with (1/2*x) in H0.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:field;auto with Geom.
IsoleVar x H0.
replace ( 0 / (1 / 2)) with 0 in H0.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;split;auto with Geom.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
assert (1/2*2=0*2).
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
ring_simplify in H2.
replace (2 * (1 / 2)) with 1 in H2.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
Qed.

Lemma weak_3_parallelogram_eq_side : forall A B C D,
   weak_3_parallelogram A B C D -> B**C= A**D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
assert (T:=H).
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
elim H;intros O HO;use HO;clear H.

assert (W0:=H0).
assert (W1:=H1).

(* Goal: @eq F (Fdiv (DSeg A D) (DSeg A B)) (Fdiv (Py P A B) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) *)
cases_equality A D.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
assert (B=C).
eauto using symmetric_point_unicity.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: not (@eq F (DSeg B C) F0) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality B C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
assert (A=D).
eauto using symmetric_point_unicity.
(* Goal: not (@eq F (DSeg P Q) F0) *)
symmetry;auto with Geom.

(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult F0 (DSeg A B)) *)
(* Goal: @eq F (Fmult (Py P A B) (DSeg A C)) (Fmult (Py P A C) (DSeg A B)) *)
cases_equality A C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq Point B C *)
(* Goal: @eq Point B C *)
assert (O=C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
use H1.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
cases_equality B D.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
assert (O=D).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in *.
(* Goal: @eq Point B C *)
use H0.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
apply (midpoint_is_midpoint) in H0.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
apply (midpoint_on_line_d) in H1.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.

assert (parallel B C A D).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (weak_3_parallelogram_parallel);auto.
cut (B**C/A**D= 1).
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
IsoleVar (B**C) H6.
rewrite H6.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

unfold is_midpoint in *.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (B ** C / A ** D) with (C**B / D**A) by auto with Geom.

cases_col C O D.
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite (elim_length_ratio_on_line_d_1 C D A O D B (0-1));auto with Geom.

replace ((C ** O / O ** D + (0 - 1)) / (D ** A / O ** D) ) with 
             ((C ** O / O ** D) / (D ** A / O ** D) + (0 - 1)/(D ** A / O ** D)).
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:field;split;unfold on_line_d in *; use H1;auto with Geom.

replace ((0 - 1) / (D ** A / O ** D)) with (D**O/D**A).
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:uniformize_dir_seg;field;split;unfold on_line_d in *; use H1;auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:assert (D<>O) by auto with Geom;auto with Geom.



unfold on_line_d in *.
(* Goal: @eq Point B C *)
use H0. use H1.
field_simplify_eq.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.

cases_equality O C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
assert (A**C=0).
apply eq_half_eq_zero.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (A=C) by auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.

assert (Col O D A).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1 O C D A);auto with Geom.

replace (D**O) with (D**A+A**O).
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:apply chasles;auto with Geom.

cut (C**O = O**A).
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
rewrite H13.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

unfold mid_point in W0.
use W0.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
rewrite H14.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite (elim_length_ratio_on_line_d_2 C D A O D B (0-1));auto with Geom.
unfold S4.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (S C O D) with (S D C O) by auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (S D O A) with (S A D O) by auto with Geom.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.

rewrite (elim_area_on_line_d D C A C O (1/2)).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
rewrite (elim_area_on_line_d A D A C O (1/2)).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S V A B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S U A B))) (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S A B V)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S A B U))) *)
uniformize_signed_areas.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
split;auto with Geom.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (Col C A D) by auto with Geom.
unfold on_line_d in *.
(* Goal: @eq Point B C *)
use H0.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (Col C A O) by auto with Geom.
assert (Col C O D).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1  C A O D);auto with Geom.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
Qed.


Lemma l3_6 : forall A B C D, 
  weak_3_parallelogram A B C D ->
 A**C * A**C + B**D * B**D = 2*A**B * A**B + 2*B**C*B**C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
cases_equality B D.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
(* Goal: per A F B *)
use H.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (DSeg D C)) (DSeg D C))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in H2.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
use H2.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
assert (D=x).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
subst x.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold mid_point in H1.
(* Goal: @eq F (Fmult (DSeg A C) (DSeg A C)) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A D)) (DSeg A D)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg C D))) (Fopp (DSeg C D)))) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
use H1.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fminus (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) (Fmult (DSeg B D) (DSeg B D)))) (Fopp (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
ring_simplify_eq.
(* Goal: @eq F (Fminus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (DSeg C D)) (DSeg C D))) F0 *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite <- (chasles A C D) in H3.
(* Goal: @eq F (Fminus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (DSeg C D)) (DSeg C D))) F0 *)
(* Goal: Col A C D *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
IsoleVar (A**C) H3.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
assert (B**C= A**D).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply weak_3_parallelogram_eq_side;auto.


(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
elim H;intros O (hA,hb);clear H.
assert (Py A O A =
       B ** O / B ** D * Py A D A + O ** D / B ** D * Py A B A -
       B ** O / B ** D * (O ** D / B ** D) * Py B D B).
apply (l3_5_py A A B D O);
(* Goal: not (@eq F (DSeg P Q) F0) *)
unfold mid_point in *;intuition;auto with Geom.
replace (B ** O / B ** D) with (1/2) in *
  by (symmetry;apply midpoint_ratio_1;auto).
replace (O ** D / B ** D)  with (1/2) in *
  by (symmetry;apply midpoint_ratio_2;auto).
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
assert (A**C = 2* A**O).
unfold  mid_point in *.
(* Goal: @eq F (DSeg A C) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
use hA.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (A**C) with (A**O + O**C) by auto with Geom.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (2 * A ** O * (2 * A ** O)) with (2*(2*A ** O * A**O)) by ring.
replace (2*A ** O * A**O) with (Py A O A) 
 by (unfold Py;uniformize_dir_seg;basic_simpl;try ring).
(* Goal: @eq F (Fplus (Fmult (Fplus F1 F1) (Py A O A)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
unfold Py;uniformize_dir_seg;basic_simpl.
(* Goal: @eq F (Fplus (Fmult (Fplus F1 F1) (Fminus (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (DSeg A D) (DSeg A D)) (Fmult (DSeg A D) (DSeg A D)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg A B) (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus F1 F1)) (Fdiv F1 (Fplus F1 F1))) (Fplus (Fmult (DSeg B D) (DSeg B D)) (Fmult (DSeg B D) (DSeg B D)))))) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
replace (A**D) with (B**C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
Qed.

Lemma l3_6_b : forall A B C D, 
  weak_3_parallelogram A B C D ->
  Py A B C = - Py B A D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C))) (Fopp (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
assert (T:=l3_6 A B C D H).
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C))) (Fopp (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
IsoleVar (A ** C * A ** C) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fminus (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) (Fmult (DSeg B D) (DSeg B D)))) (Fopp (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
ring_simplify_eq.
(* Goal: @eq F (Fplus (Fmult (Fopp (DSeg B C)) (DSeg B C)) (Fmult (DSeg A D) (DSeg A D))) F0 *)
replace (B**C) with (A**D).
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
symmetry;
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply weak_3_parallelogram_eq_side;auto.
Qed.


Lemma l_27_c : forall A B C D P Q, weak_3_parallelogram A B C D ->
Py P A Q + Py P C Q = Py P B Q + Py P D Q + 2 * Py B A D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
assert (X:= H).
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
unfold weak_3_parallelogram in H.
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
elim H; intros O HO; clear H.
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
use HO.
assert (T:= l_28_b_midpoint O A C P Q H).
assert (U:= l_28_b_midpoint O B D P Q H0).
(* Goal: @eq F (Fplus (Py A P Q) (Py C P Q)) (Fplus (Py B P Q) (Py D P Q)) *)
assert (Py P A Q + Py P C Q - 1 / 2 * Py A C A =  Py P B Q + Py P D Q - 1 / 2 * Py B D B) by congruence.
clear T U.
assert (2* Py B A D =  1/2 * (Py A C A - Py B D B)).
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (2 * Py B A D) with (Py B A D + Py B A D) by ring.
replace (Py B A D) with (- Py A B C).
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
uniformize_dir_seg;basic_simpl.
field_simplify_eq.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fminus (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) (Fmult (DSeg B D) (DSeg B D)))) (Fopp (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A D) (DSeg A D))) (Fmult (DSeg B D) (DSeg B D)))) *)
ring_simplify_eq.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.
assert (T:=l3_6 A B C D X).
IsoleVar (B ** D * B ** D) T.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (2 * B ** D * B ** D) with (2 * (B ** D * B ** D)) by ring.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
assert (U:=l3_6_b A B C D X).
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
rewrite U;ring.

(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
IsoleVar (Py P A Q + Py P C Q) H1.
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma l3_8_a : forall A B C D P, weak_3_parallelogram A B C D ->
Py P A B = Py4 P D A C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py4 P D A C) with (Py4 C A D P) by auto with Geom.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.
(* Goal: @eq F (Py P A B) (Fminus (Py C A P) (Py D A P)) *)
assert (T:=l_27_a A B C D A P H).
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (Fminus (Py A C D) (Py B C D)) (Fminus F0 (Py D C D))) (Fdiv (Fminus (Py A C D) (Py B C D)) (Fopp (Py C D C))) *)
(* Goal: not (perp C D C D) *)
uniformize_pys.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
Qed.

Lemma l3_8_b : forall A B C D P, weak_3_parallelogram A B C D ->
Py P A B = Py P D C - Py A D C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite (l3_8_a A B C D) by auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma l_28_a : forall A B U V Y,
Col Y U V -> U <> V ->
S A B Y = U**Y/U**V * S A B V + Y**V/U**V * S A B U.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (S A B Y) with (S Y A B) by auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite (l2_9 A B U V Y) by auto.
(* Goal: @eq F (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S V A B)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S U A B))) (Fplus (Fmult (Fdiv (DSeg U Y) (DSeg U V)) (S A B V)) (Fmult (Fdiv (DSeg Y V) (DSeg U V)) (S A B U))) *)
uniformize_signed_areas.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.

Lemma on_foot_per : forall A B C F, 
  on_foot F A B C ->
  per A F B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: per A F B *)
unfold on_foot in H.
(* Goal: per A F B *)
use H.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (perp A F B C) by auto with Geom.
(* Goal: per A F B *)
cut (perp A F F B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: perp A F F B *)
cut (perp F B A F).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_para_perp B C A F F B);auto with Geom.
Qed.

Lemma herron_qin : forall A B C,
S A B C * S A B C = 1 / (2*2*2*2) * (Py A B A * Py A C A - Py B A C * Py B A C).
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (@eq F (DSeg B C) F0) *)
(* Goal: @eq F (Fdiv (Py P A B) (Py P A C)) (Fdiv (DSeg A B) (DSeg A C)) *)
cases_equality B C.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Fminus (Py A C D) (Py B C D)) (Fminus F0 (Py D C D))) (Fdiv (Fminus (Py A C D) (Py B C D)) (Fopp (Py C D C))) *)
(* Goal: not (perp C D C D) *)
uniformize_pys.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

elim (proj_ex A B C H).
intros F HF.

cases_equality B F.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
assert (T:=on_foot_area A F C F HF).
field_simplify_eq.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:repeat apply nonzeromult;auto with Geom.
replace (2 * (2 * (2 * 2)) * S A F C * S A F C) with
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
(2*2*(2 * 2 * S A F C * S A F C)) by ring.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.

unfold on_foot in HF.
use HF.
clear H2 H3.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (perp F C A F) by auto with Geom.
(* Goal: not (perp A B A B) *)
unfold perp, Py4 in *.
IsoleVar (Py C A F) H1.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py C A F) with (Py F A C) in H1 by auto with Geom.
(* Goal: @eq F (DSeg A I) (Fmult (Fdiv F1 (Fplus F1 F1)) (DSeg A B)) *)
(* Goal: not (@eq F (DSeg A B) F0) *)
rewrite H1.
(* Goal: @eq F (Fdiv (Fminus (Py A C D) (Py B C D)) (Fminus F0 (Py D C D))) (Fdiv (Fminus (Py A C D) (Py B C D)) (Fopp (Py C D C))) *)
(* Goal: not (perp C D C D) *)
uniformize_pys.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.

assert (Py A C A = Py A F A + Py F C F).
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (A ** C * A ** C + A ** C * A ** C) with (2*(A**C*A**C)) by ring.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (A ** F * A ** F + A ** F * A ** F) with (2*(A ** F * A ** F)) by ring.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (C ** F * C ** F + C ** F * C ** F) with (2*(C**F*C**F)) by ring.
replace ( 2 * (A ** F * A ** F) + 2 * (C ** F * C ** F))
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
with (2*(A ** F * A ** F + C ** F * C ** F)) by ring.
assert (A ** C * A ** C = A ** F * A ** F + C ** F * C ** F).
assert (Py A F C = 0).
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace 0 with (-0) by ring.
rewrite <- H0.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
unfold Py in H2.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
IsoleVar (A ** F * A ** F + C ** F * C ** F) H2.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite H2;auto.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

assert (Col B F C).
unfold on_foot in HF.
(* Goal: not (@eq F (DSeg P Q) F0) *)
use HF;auto with Geom.
assert (T:= l_3_4_b B F C A H1).
replace (Py A B F) with (Py F B F) in T.

replace (Py F B F) with (2*B**F*B**F) in T.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
2:unfold Py;uniformize_dir_seg;basic_simpl;ring.
IsoleVar (Py A B C) T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.

replace (2 * B ** F * B ** F * B ** C / B ** F) with 
 ( 2 * B ** F * B ** C) in T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:field;auto with Geom.

replace (S A B C * S A B C) with (1/2 *1/2*A**F*A**F*B**C*B**C).
2: replace (1 / 2 * 1/2*A**F*A**F*B**C* B ** C ) with 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
               (1/2 * 1/2 *  (A ** F * A**F * B ** C *B**C )) by ring.
2: (rewrite <- on_foot_area).
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:field;auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto.


replace ( 1 / 2 * 1/2 *  A ** F * A ** F * B ** C * B**C ) with
((1/2)* (A**F * A**F) * (1/2)* (B**C * B**C))
   by (field;solve_conds;auto with Geom).

replace (A**F * A**F) with (A**B * A**B - B**F * B**F).
field_simplify_eq.
replace (2 * (2 * (2 * 2)) * B ** F * B ** F * B ** C * B ** C) 
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
with ( 2 * 2 * (2*B ** F *B ** C) * (2*B ** F * B ** C)) by ring. 
rewrite <- T.
(* Goal: @eq F (Py A B C) (Fopp (Py B A D)) *)
unfold Py.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
solve_conds.

assert (per A F B).
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (on_foot_per A B C F);auto.
unfold per,Py in *.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
IsoleVar (A**B*A**B) H3.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

assert (per A F B).
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
apply (on_foot_per A B C F);assumption.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
unfold Py;uniformize_dir_seg;basic_simpl.
unfold per, Py in H2.
IsoleVar (A**B*A**B) H2.
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H2.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.

Qed.

Lemma l3_9_aux : forall B D P Q R S Y ,
 Col Y B D ->
 B<>D ->
 B ** Y = Q ** S ->
 weak_3_parallelogram B Y S Q ->
 Py4 P Q R S = Q ** S / B ** D * Py4 P B R D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py D C D) (Fopp F0) *)
(* Goal: False *)
rewrite <- H1.
replace (Py4 P Q R S) with (Py4 P B R Y).

(* Goal: not (@eq F (DSeg P Q) F0) *)
2:replace (Py4 P B R Y) with (Py4 B P Y R) by auto with Geom.
2:rewrite (l_27_b B Y S Q P R H2).
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.

(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.

assert ( Py P B Y * B ** D = Py P B D * B ** Y).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (l_3_4_b B Y D P); auto with Geom.
IsoleVar (Py P B Y) H3.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.
(* Goal: @eq F (Fplus (DSeg A O) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg A O)) *)
(* Goal: @eq F (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg B D) (DSeg B D))) (Fplus (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))) *)
rewrite H3.
assert (Py R B Y * B ** D = Py R B D * B ** Y).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (l_3_4_b  B Y D R);auto with Geom.
IsoleVar (Py R B Y) H5.
rewrite H5.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.
Qed.

Lemma l3_9 : forall P Q R S A B C D,
  parallel P R A C ->
  parallel Q S B D ->
  B<>D -> A<>C -> ~ perp A C B D ->
  Py4 P Q R S / Py4 A B C D = (P**R / A**C) * (Q**S / B**D).
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
assert (exists Y : Point,
         Col Y A C /\ A ** Y = P ** R /\ weak_3_parallelogram A Y R P).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (on_line_dex_spec_strong_f A C P R);auto with Geom.
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
elim H4;intros X HX;clear H4; use HX.
assert (exists Y : Point,
         Col Y B D /\ B ** Y = Q ** S /\ weak_3_parallelogram B Y S Q).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (on_line_dex_spec_strong_f B D Q S);auto with Geom.
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
elim H5;intros Y HY;clear H5; use HY.

assert (Ha:Py4 P Q R S  = Q**S / B**D * Py4 P B R D).

(* Goal: not (@eq F (DSeg P Q) F0) *)
eapply l3_9_aux with (Y:=Y); auto with Geom.

assert (Hb:Py4 P B R D  = P**R / A**C * Py4 A B C D).

(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py4 P B R D) with (Py4 B P D R) by auto with Geom.
(* Goal: @eq F (Py4 B P D R) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Py4 A B C D)) *)
(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite (l3_9_aux A C B P D R X H4 H2 H6 H7).
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py4 B A D C) with (Py4 A B C D) by auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;auto with Geom.

(* Goal: @eq F (Fdiv (Py4 P Q R S) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Ha.
(* Goal: @eq F (Fdiv (Fmult (Fdiv (DSeg Q S) (DSeg B D)) (Py4 P B R D)) (Py4 A B C D)) (Fmult (Fdiv (DSeg P R) (DSeg A C)) (Fdiv (DSeg Q S) (DSeg B D))) *)
rewrite Hb.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;solve_conds;auto with Geom.
Qed.


Lemma l3_10 : forall A B C D,
 parallel A B C D ->
 C<>D ->
 A**B/C**D = Py4 A C B D / - Py C D C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
replace (A ** B / C ** D) with ((A ** B / C ** D) * (C**D / C**D))
 by (field;auto with Geom).
(* Goal: not (@eq F (DSeg P Q) F0) *)
rewrite <- (l3_9 A C B D C C D D);auto with Geom.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Fminus (Py A C D) (Py B C D)) (Fminus F0 (Py D C D))) (Fdiv (Fminus (Py A C D) (Py B C D)) (Fopp (Py C D C))) *)
(* Goal: not (perp C D C D) *)
uniformize_pys.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (Fopp (Py C D C)) F0) *)
(* Goal: not (perp C D C D) *)
cut (Py C D C <> 0).
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (perp C D C D) *)
unfold perp, Py4.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
assert (Py D C D = 0).
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (0) with (-0) by ring.
(* Goal: @eq F (Py D C D) (Fopp F0) *)
(* Goal: False *)
rewrite <- H1.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
ring.
(* Goal: False *)
assert (D=C).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
Qed.

Lemma l3_10b : forall A B C D,
 parallel A B C D ->
 C<>D ->
 A**B/C**D = Py4 B C A D / Py C D C.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
rewrite l3_10 by assumption.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py4 B C A D) with (- Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
split;auto with Geom.
Qed.

Lemma perp_not_parallel : forall A B C D,
  perp A B C D ->
  A <> B -> C <> D ->
  ~ parallel A B C D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Py P A B) F0 *)
unfold perp in H.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
assert (T:=l3_10 A B C D H2 H1).
rewrite H in T.
IsoleVar (A**B) T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
2:auto with Geom.
replace (C ** D * (0 / - Py C D C)) with 0 in T.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (A=B) by auto with Geom.
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
(* Goal: @eq F (Fmult (Fplus F1 F1) (Py P O Q)) (Fminus (Fplus (Py P A Q) (Py P B Q)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A B A))) *)
subst A.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
cut (Py C D C <>  0).
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma not_perp_to_itself : forall A B,
A <> B ->~ perp A B A B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (perp A B A B) *)
unfold perp, Py4 in *.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
IsoleVar (Py B A B) H0.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: False *)
assert (A=B).
(* Goal: @eq Point A B *)
(* Goal: False *)
unfold Py in *.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
replace (A ** B * A ** B + A ** B * A ** B) with (2*(A ** B * A ** B)) in * by ring.
(* Goal: @eq Point A B *)
(* Goal: False *)
IsoleVar (A ** B) H0.
(* Goal: @eq Point A B *)
(* Goal: not (@eq F (DSeg A B) F0) *)
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
(* Goal: False *)
replace (0 / 2 / A ** B) with 0 in *.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
split;auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
Qed.

Lemma parallel_not_perp : forall A B C D,
  parallel A B C D ->
  A <> B -> C <> D ->
  ~ perp A B C D.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.
(* Goal: False *)
assert (perp C D C D).
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
apply (perp_para_perp A B C D C D);assumption.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (not_perp_to_itself C D);auto.
Qed.



Lemma l_25_a : forall A B P Q Y,
  P<>Q -> Q<>Y -> Py Q A B <> 0 ->
 on_inter_line_perp Y A P Q A B ->
 P**Y / Q**Y = Py P A B / Py Q A B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold on_inter_line_perp in *.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
use H2.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
assert (A<>B).
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro;subst;basic_simpl;intuition.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
elim (proj_ex P A B H2).
(* Goal: forall (x : Point) (_ : on_foot x P A B), @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
intros P1 HP1.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
unfold on_foot in *.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
use HP1.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
elim (proj_ex Q A B H2).
(* Goal: forall (x : Point) (_ : on_foot x Q A B), @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
intros P2 HP2.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
unfold on_foot in *.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
use HP2.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
assert (Pa:=H5).
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
assert (Pb:=H4).
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
assert (Pc:=H7).
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
unfold perp, Py4 in H4, H5, H7.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
IsoleVar (Py P A B) H4.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
IsoleVar (Py Q A B) H7.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Py P A B) (Py Q A B)) *)
rewrite H4, H7.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
rewrite col_pyth by assumption.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (Fmult (Fmult (Fplus F1 F1) (DSeg A P1)) (DSeg A B)) (Py P2 A B)) *)
assert (A<>P2).
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro;subst;basic_simpl;intuition.
(* Goal: Col Y U V *)
(* Goal: @eq F (Py A Y B) (Fminus (Fplus (Fmult r1 (Py A V B)) (Fmult r2 (Py A U B))) (Fmult (Fmult r1 r2) (Py U V U))) *)
rewrite col_pyth by assumption.
replace (2 * A ** P1 * A ** B / (2 * A ** P2 * A ** B)) with (A**P1/A**P2)
 by (field;repeat split;auto with Geom).

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (parallel P P1 Y A).
(* Goal: parallel P P1 Y A *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (T:=perp_perp_para Y A A B P1 P H12 Pa Pb).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (parallel Y A Q P2).
(* Goal: parallel Y A Q P2 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
apply (perp_perp_para Y A A B Q P2 H12 Pa).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* ici *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cases_equality A Y.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
clear H13 H14 Pa H5 H9 H12.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (parallel P1 P P2 Q).
(* Goal: parallel P1 P P2 Q *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
apply (perp_perp_para P1 P Y B P2 Q H2 Pb Pc).


(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cases_col Y Q P2.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
rename H9 into HCol.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (parallel P Q P2 Q).
(* Goal: parallel Y B P1 P *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
unfold parallel, S4.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.

(* Goal: @eq F (S P P2 Q) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (Col Q P P2).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1 Q Y P P2);auto with Geom.
(* Goal: @eq F (S P P2 Q) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (Col P P2 Q).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cases_equality P2 Q.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
clear H9 H5 H7 Pc.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (Col Y P B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1 Y Q P B);auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (parallel P1 P Y B).
(* Goal: parallel P1 P Y B *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cut (parallel Y B P1 P).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: parallel Y B P1 P *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
unfold parallel, S4.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (Col Y B P) by auto with Geom.
(* Goal: @eq F (Fplus (S Y P1 B) (S Y B P)) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
rewrite H7.
(* Goal: @eq F (Fplus (S Y P1 B) F0) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
basic_simpl.
(* Goal: @eq F (S Y P1 B) F0 *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (Col Y P1 B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cases_equality P1 P.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
subst.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;split;auto with Geom.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y Q)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
cut False.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.

(* Goal: False *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
apply parallel_not_perp in H7.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (perp P Q Y B).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_para_perp P2 Q  Y B P Q);auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
assert (perp Y B P Q) by auto with Geom.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.



(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
assert (Y ** P / Y ** Q = Y ** P1 / Y ** P2).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (thales_2 Y Q P P2 P1);auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1 Y B P2 P1);auto with Geom.
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg Y P1) (DSeg Y P2)) *)
(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
rewrite <- H12.
(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
(* Goal: not (@eq F (DSeg P Q) F0) *)
field;split;auto with Geom.


(* Goal: @eq F (Fdiv (DSeg P Y) (DSeg Q Y)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
rewrite (l1_25 P Y Q P1 A P2).

(* Goal: @eq F (Fdiv (DSeg P1 A) (DSeg P2 A)) (Fdiv (DSeg A P1) (DSeg A P2)) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
uniformize_dir_seg.
field;solve_conds.
(* Goal: not (@eq F (Fopp (DSeg P2 A)) F0) *)
(* Goal: not (@eq F (DSeg P2 A) F0) *)
(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
cut (P2**A<>0).
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.

(* Goal: not (Col Q Y A) *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intro.

(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
assert (per B A Q).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (perp_col_perp B A Y Q); auto with Geom.
(* Goal: per B A Y *)
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
unfold per.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py B A Y) with (Py Y A B) by auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
unfold per in H17.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (Py B A Q) with (Py Q A B) in H17 by auto with Geom.
(* Goal: False *)
(* Goal: Col P Y Q *)
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
intuition.

(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: Col P1 A P2 *)
(* Goal: parallel P P1 Y A *)
(* Goal: parallel Y A Q P2 *)
assert (Col A P1 P2).
(* Goal: not (@eq F (DSeg P Q) F0) *)
apply (col_trans_1 A B P1 P2);auto with Geom.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
Qed.

Lemma l_25_b : forall A B P Q Y,
  P<>Q -> Q<>Y -> Py Q A B <> 0 ->
 on_inter_line_perp Y A P Q A B ->
 P**Y / P**Q = Py P A B / Py4 P A Q B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
assert (T:= l_25_a A B P Q Y H H0 H1 H2).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold on_inter_line_perp in *.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
use H2.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (P**Y) with (P**Q + Q**Y) in T by auto with Geom.
replace ((P ** Q + Q ** Y) / Q ** Y) with (P**Q/Q**Y + 1) in T 
  by (field;auto with Geom).
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (P**Y) with (P**Q + Q**Y) by auto with Geom.

replace ((P ** Q + Q ** Y) / P ** Q) with (Q**Y/P**Q + 1) 
  by (field;auto with Geom).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
IsoleVar (Py P A B) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto with Geom.
replace (Py Q A B * (P ** Q + Q ** Y) - Py Q A B * Q ** Y) with
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
(Py Q A B *  (P ** Q)) by ring.
(* Goal: not (@eq F (Fmult (Py Q A B) (DSeg P Q)) F0) *)
apply nonzeromult.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

Lemma l_25_c : forall A B P Q Y,
  P<>Q -> Q<>Y -> Py Q A B <> 0 ->
 on_inter_line_perp Y A P Q A B ->
 Q**Y / P**Q = Py Q A B / Py4 P A Q B.
Proof.
(* Goal: forall (A B P Q Y : Point) (_ : not (@eq Point P Q)) (_ : not (@eq Point Q Y)) (_ : not (@eq F (Py Q A B) F0)) (_ : on_inter_line_perp Y A P Q A B), @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
assert (T:= l_25_a A B P Q Y H H0 H1 H2).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold on_inter_line_perp in *.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
use H2.
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (P**Y) with (P**Q + Q**Y) in T by auto with Geom.
replace ((P ** Q + Q ** Y) / Q ** Y) with (P**Q/Q**Y + 1) in T 
  by (field;auto with Geom).
(* Goal: not (@eq F (DSeg P Q) F0) *)
replace (P**Y) with (P**Q + Q**Y) by auto with Geom.

replace ((P ** Q + Q ** Y) / P ** Q) with (Q**Y/P**Q + 1) 
  by (field;auto with Geom).
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Py4 P A Q B)) *)
unfold Py4.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
IsoleVar (Py P A B) T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Py P A B) (Py Q A B))) *)
rewrite T.
(* Goal: @eq F (Fdiv (DSeg Q Y) (DSeg P Q)) (Fdiv (Py Q A B) (Fminus (Fmult (Py Q A B) (Fplus (Fdiv (DSeg P Q) (DSeg Q Y)) F1)) (Py Q A B))) *)
field.
(* Goal: not (@eq F (DSeg P Q) F0) *)
repeat split;auto with Geom.
replace (Py Q A B * (P ** Q + Q ** Y) - Py Q A B * Q ** Y) with
(* Goal: @eq F (Py D C D) (Fopp (Fminus F0 (Py D C D))) *)
(* Goal: False *)
(Py Q A B *  (P ** Q)) by ring.
(* Goal: not (@eq F (Fmult (Py Q A B) (DSeg P Q)) F0) *)
apply nonzeromult.
(* Goal: not (@eq F (Py Q A B) F0) *)
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto.
(* Goal: not (@eq F (DSeg P Q) F0) *)
auto with Geom.
Qed.

