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

Set Nested Proofs Allowed.
Require Export area_elimination_lemmas.
Require Import Classical.

(** For the first time, we need decidability of the parallel predicate *)

Lemma parallel_dec : forall A B C D, parallel A B C D \/ ~ parallel A B C D.
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: or (parallel A B C D) (not (parallel A B C D)) *)
apply classic.
Qed.

(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
Ltac cases_parallel A B C D := elim (parallel_dec A B C D);intros.

Definition Det3 (x1 x2 x3 y1 y2 y3 z1 z2 z3 : F) : F :=
  x1 * (y2 * z3) - x1 * (y3 * z2) - x2 * (y1 * z3) + x2 * (y3 * z1) +
  x3 * (y1 * z2) - x3 * (y2 * z1).

Lemma freepoint_elimination_aux : forall O U V B Y:Point, ~ Col O U V ->
S O B Y = 1/ (S O U V) * (S O B V * S O U Y + S O B U * S O Y V).
Proof with Geometry.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.

cases_parallel U V O Y.
rename H into T.
assert (O**Y / U**V = S U O Y / S O V U).
apply l2_15...
assert (S O B Y = S O B O + (O**Y/U**V) * S4 O U B V).
apply elim_area_on_parallel.
unfold on_parallel;repeat split...
eauto with Geom.
rewrite H in H1.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
unfold S4 in *.
assert (parallel O Y U V).
Geometry.
unfold parallel, S4 in *.
IsoleVarRing (S O Y V) H2.
rewrite H2.
rewrite H1.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
split...

assert (exists W, inter_ll W U V O Y).
apply inter_ll_ex...
DecompEx H1 W.

cases_equality W O.
subst W.
unfold inter_ll in *.
(* Goal: False *)
intuition.
rename H1 into Hdiff.

assert (S B O W = 1 / S4 U O V Y * (S U O Y * S B O V + S V Y O * S B O U)).
apply  elim_area_inter_ll...
replace (S4 U O V Y) with (- S4 O U Y V) in H1.
2:Geometry.
replace ((S U O Y * S B O V + S V Y O * S B O U)) with 
(S O B V * S O U Y + S O B U * S O Y V) in H1.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
2:uniformize_signed_areas;field.
unfold inter_ll in *;DecompAndAll.
assert (O ** W / O ** Y = S O U V / S4 O U Y V).
apply co_side_ter...
cases_col B O W.

cases_equality V W.
subst W.
assert (Col O Y B).
eapply col_trans_1 with (B:=V)...
unfold Col in *.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
rewrite H4.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
rewrite H5.
rewrite H7.
ring.

cases_equality O B.
subst B.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
ring.

cases_col  V O B.
assert (Col O Y B).
eapply col_trans_1 with (B:= W)...
assert (Col O Y V).
eapply col_trans_1 with (B:= B)...
unfold Col in *.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S U C O)) (Fopp (S U O D)))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
rewrite H9.
rewrite H10.
rewrite H11.
ring.

assert (U**W/V**W = S U O B / S V O B).
apply co_side...

cases_col V O Y.

cases_equality Y O.
subst Y.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
ring.

assert (Col Y W V).
eapply col_trans_1 with (B:= O)...
assert (Col W U Y).
eapply col_trans_1 with (B:= V)...

cases_equality Y W.
Unset Regular Subst Tactic.
subst W.
Set Regular Subst Tactic.
clear H13 H12 H5.
assert (Col O V B).
eapply col_trans_1 with (B:= Y)...
unfold Col in *.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
rewrite H4.
replace (S V O B) with (-0).
rewrite H11.
ring.
rewrite <- H5.
ring.

assert (Col Y U O).
eapply col_trans_1 with (B:= W)...
assert (Col O U V).
eapply col_trans_1 with (B:= Y)...
(* Goal: False *)
intuition.

assert (U**W/V**W = S U O Y / S V O Y).
apply co_side...
rewrite H10 in H12.

assert (Col O B Y).
eapply col_trans_1 with (B:= W)...
rewrite H13.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
RewriteVar (S O B U) H12.
2:Geometry.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
split...

(** Second case *)
assert (O**Y / O**W = S B O Y / S B O W).
apply A6...
assert (O**Y / O**W = S4 O U Y V / S O U V).
replace (O ** Y / O ** W) with (1/(O ** W / O ** Y)). 
rewrite H2.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
Geometry.
repeat apply nonzeromult...
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
split...
unfold not;intro.
assert (O=Y).
Geometry.
subst Y.
assert (parallel U V O O)...
rewrite H7 in H8.
set (S O B V * S O U Y + S O B U * S O Y V) in *.
rewrite H1 in H8.
replace (S B O Y) with (-S O B Y) in H8.
2:Geometry.

RewriteVar (S O B Y) H8.
field;split...
apply nonzeromult...
apply nonzerodiv...

unfold not;intro.
rewrite H9 in H1.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
assert (Col O Y B).
eapply col_trans_1 with (B:=W)...
Geometry.

Qed.




Lemma  free_points_area_elimination :
    forall O U V A B Y : Point, 
    S O U V <> 0 ->
    S A B Y =
    Det3 (S O U A) (S O V A) 1 (S O U B) (S O V B) 1 (S O U Y) (S O V Y) 1 /
    S O U V.
Proof with Geometry.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
unfold Det3.
replace (S A B Y) with (S A B O + S A O Y + S O B Y)...

replace (S A O Y) with (- S O A Y).
2:symmetry;Geometry.
replace (S O A Y) with (1/ (S O U V) * (S O A V * S O U Y + S O A U * S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S O B Y) with (1/ (S O U V) * (S O B V * S O U Y + S O B U * S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S A B O) with (S O A B).
2:Geometry.
replace (S O A B) with (1/ (S O U V) * (S O A V * S O U B + S O A U * S O B V)).
2:symmetry;eapply freepoint_elimination_aux...
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
uniformize_signed_areas.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field...
Qed.

Lemma free_points_ratio_elimination_1 : forall O U V A B C D : Point,
  parallel A B C D ->
  C<>D ->
  S O U V <> 0 ->
  S U A B <> 0 ->
  A**B / C**D = (S O U A * S O V B + S O U A * S O U V - S O V A * S O U B -
 S O U B * S O U V) /
(S O U A * S O V D - S O U A * S O V C + S O V A * S O U C -
 S O V A * S O U D + S O U V * S O U C - S O U V * S O U D).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.

(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
cases_equality A B.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
subst.
(* Goal: False *)
basic_simpl;intuition.

assert (A**B / C**D = (S O A B + S O U A - S O U B) / (S U C D - S A C D)
 /\ (S U C D - S A C D) <> 0 ).
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   elim (on_line_dex_spec_strong_f A B C D H H3).
(* Goal: forall (x : Point) (_ : and (Col x C D) (and (@eq F (DSeg C x) (DSeg A B)) (weak_3_parallelogram C x B A))), and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   intros D' Hn. decompose [and] Hn;clear Hn.
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   rewrite <- H6.
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   assert (A<>D').
(* Goal: not (@eq Point C D') *)
(* Goal: and (@eq F (Fdiv (DSeg C D') (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   intro;subst; basic_simpl; auto with Geom.
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   assert (~ Col U A D').
(* Goal: not (Col O C D) *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
     intro.
(* Goal: False *)
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
     assert (Col A B U).
       eapply (col_trans_1);eauto with Geom.
(* Goal: False *)
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
       assert (Col U A B); auto with Geom.

(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   rewrite (A6 A B D' U H5 H8) by auto with Geom.

(* Goal: and (@eq F (Fdiv (S U A B) (S U A D')) (Fdiv (Fminus (Fplus (S O A B) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D)))) (not (@eq F (Fminus (S U C D) (S A C D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   rewrite (A5 U A B O).
   assert (S U A D' = S U C D - S A C D) by
     (apply (l2_12a_strong_3 A D' D C U);auto).
(* Goal: and (@eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   split.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   uniformize_signed_areas.
(* Goal: @eq F (Fdiv (Fplus (Fplus (S U A O) (S U O B)) (S O A B)) (S U A D')) (Fdiv (Fminus (Fplus (S O A B) (S U A O)) (Fopp (S U O B))) (Fminus (S U C D) (S A C D))) *)
(* Goal: not (@eq F (Fminus (S U C D) (S A C D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   rewrite H9; field; rewrite <- H9; auto with Geom.
(* Goal: not (@eq F (Fminus (S U C D) (S A C D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
   rewrite <- H9;auto with Geom.   

(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
use H4.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
rewrite H5.
(* Goal: @eq F (Fdiv (S O A B) (S O C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
rewrite (free_points_area_elimination O U V O A B) in * by assumption.
(* Goal: @eq F (Fdiv (Fminus (Fplus (Fdiv (Det3 (S O U O) (S O V O) F1 (S O U A) (S O V A) F1 (S O U B) (S O V B) F1) (S O U V)) (S O U A)) (S O U B)) (Fminus (S U C D) (S A C D))) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
rewrite (free_points_area_elimination O U V U C D) in * by assumption.
(* Goal: @eq F (Fdiv (Fminus (Fplus (Fdiv (Det3 (S O U O) (S O V O) F1 (S O U A) (S O V A) F1 (S O U B) (S O V B) F1) (S O U V)) (S O U A)) (S O U B)) (Fminus (Fdiv (Det3 (S O U U) (S O V U) F1 (S O U C) (S O V C) F1 (S O U D) (S O V D) F1) (S O U V)) (S A C D))) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O U A) (S O V B)) (Fmult (S O U A) (S O U V))) (Fmult (S O V A) (S O U B))) (Fmult (S O U B) (S O U V))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D)))) *)
rewrite (free_points_area_elimination O U V A C D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
replace (S O V U) with (- S O U V) in * by auto with Geom.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: and (not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0)) (not (@eq F (S O U V) F0)) *)
split;auto.
(* Goal: not (@eq F (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V))) F0) *)
clear H5.
replace ((0 - - (S O U V * S O U C) - S O U V * S O U D + S O U C * S O V D -
      S O V C * S O U D) / S O U V -
     (S O U A * S O V C - S O U A * S O V D - S O V A * S O U C +
      S O V A * S O U D + S O U C * S O V D - S O V C * S O U D) / S O U V
)
with ((0 - - (S O U V * S O U C) - S O U V * S O U D + S O U C * S O V D -
      S O V C * S O U D - (S O U A * S O V C - S O U A * S O V D - S O V A * S O U C +
      S O V A * S O U D + S O U C * S O V D - S O V C * S O U D)) / S O U V) in H6 by (field;auto).
replace (0 - - (S O U V * S O U C) - S O U V * S O U D + S O U C * S O V D -
      S O V C * S O U D -
      (S O U A * S O V C - S O U A * S O V D - S O V A * S O U C +
       S O V A * S O U D + S O U C * S O V D - S O V C * S O U D)) with (S O U A * S O V D - S O U A * S O V C + S O V A * S O U C - S O V A * S O U D +
S O U V * S O U C - S O U V * S O U D) in H6 by ring.
(* Goal: not (@eq F (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U A) (S O V D)) (Fmult (S O U A) (S O V C))) (Fmult (S O V A) (S O U C))) (Fmult (S O V A) (S O U D))) (Fmult (S O U V) (S O U C))) (Fmult (S O U V) (S O U D))) F0) *)
intro Hx; rewrite Hx in H6; clear Hx.
basic_simpl;
(* Goal: False *)
intuition.
Qed.


Lemma free_point_ratio_elimination_2 : forall O U V A B C D : Point,
  parallel A B C D ->
  C<>D ->
  S O U V <> 0 ->
  S V A B <> 0 ->
  A**B / C**D = (S O V A * S O U B + S O V A * S O V U - S O U A * S O V B -
 S O V B * S O V U) /
(S O V A * S O U D - S O V A * S O U C + S O U A * S O V C -
 S O U A * S O V D + S O V U * S O V C - S O V U * S O V D).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) *)
assert (S O V U <> 0).
(* Goal: not (@eq F (S O V U) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O V A) (S O U B)) (Fmult (S O V A) (S O V U))) (Fmult (S O U A) (S O V B))) (Fmult (S O V B) (S O V U))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V A) (S O U D)) (Fmult (S O V A) (S O U C))) (Fmult (S O U A) (S O V C))) (Fmult (S O U A) (S O V D))) (Fmult (S O V U) (S O V C))) (Fmult (S O V U) (S O V D)))) *)
intro; apply H1;uniformize_signed_areas;auto with Geom.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fminus (Fplus (Fmult (S O V A) (S O U B)) (Fmult (S O V A) (S O V U))) (Fmult (S O U A) (S O V B))) (Fmult (S O V B) (S O V U))) (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V A) (S O U D)) (Fmult (S O V A) (S O U C))) (Fmult (S O U A) (S O V C))) (Fmult (S O U A) (S O V D))) (Fmult (S O V U) (S O V C))) (Fmult (S O V U) (S O V D)))) *)
rewrite (free_points_ratio_elimination_1 O V U A B C D) by auto.
(* Goal: @eq F (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) *)
reflexivity.
Qed.

Lemma free_points_ratio_elimination_3 : forall O U V A B C D : Point,
  parallel A B C D ->
  A<>B ->
  C<>D ->
  S O U V <> 0 ->
  S U C D <> 0 ->
  A**B / C**D = (S O U C * S O V B - S O U C * S O V A + S O V C * S O U A -
  S O V C * S O U B + S O U V * S O U A - S O U V * S O U B)/
  (S O U C * S O V D + S O U C * S O U V - S O V C * S O U D -
  S O U D * S O U V).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
assert (A**B / C**D =  (S U A B - S C A B) / (S O C D + S O U C - S O U D) 
 /\ (S O C D + S O U C - S O U D) <> 0 ).
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
assert (parallel C D A B) by auto with Geom.
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   elim (on_line_dex_spec_strong_f C D A B H4 H1).
(* Goal: forall (x : Point) (_ : and (Col x C D) (and (@eq F (DSeg C x) (DSeg A B)) (weak_3_parallelogram C x B A))), and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   intros D' Hn. decompose [and] Hn;clear Hn.
(* Goal: and (@eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite <- H7.
(* Goal: and (@eq F (Fdiv (DSeg C D') (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   assert (C<>D').
(* Goal: not (@eq Point C D') *)
(* Goal: and (@eq F (Fdiv (DSeg C D') (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   intro;subst; basic_simpl; auto with Geom.

(* Goal: and (@eq F (Fdiv (DSeg C D') (DSeg C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite (A6 C D' D U H1) by auto with Geom.
(* Goal: and (@eq F (Fdiv (S U C D') (S U C D)) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite (A5 U C D O).
(* Goal: and (@eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   assert (T:=A5 U C D O).
   assert (S U C D' = S U A B - S C A B) by
     (apply (l2_12a_strong_3 C D' B A U);auto).
(* Goal: and (@eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   split.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   uniformize_signed_areas.
(* Goal: @eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S U C O)) (Fopp (S U O D)))) *)
(* Goal: not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite H9.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
   field.
   replace (S O C D + S U C O - - S U O D) 
      with (S U C O + S U O D + S O C D) by ring.
(* Goal: not (@eq F (Fplus (Fplus (S U C O) (S U O D)) (S O C D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite <- T;auto.
   replace (S O C D + S O U C - S O U D) 
      with (S U C O + S U O D + S O C D)
        by (uniformize_signed_areas;ring).
(* Goal: not (@eq F (Fplus (Fplus (S U C O) (S U O D)) (S O C D)) F0) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
   rewrite <- T;auto.

(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
use H4.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
rewrite H5.
(* Goal: @eq F (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
rewrite (free_points_area_elimination O U V U A B) in * by assumption.
(* Goal: @eq F (Fdiv (S C A B) (S A D C)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
rewrite (free_points_area_elimination O U V C A B) in * by assumption.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
rewrite (free_points_area_elimination O U V O C D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
replace (S O V U) with (- S O U V) in * by auto with Geom.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: and (not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0)) (not (@eq F (S O U V) F0)) *)
split;auto.
(* Goal: not (@eq F (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V))) F0) *)
clear H5.

replace ((S O U C * S O V D - S O V C * S O U D) / S O U V + S O U C - S O U D)
with ((S O U C * S O V D + S O U C * S O U V - S O V C * S O U D - S O U D * S O U V) / (S O U V))
in H6 by (field;auto).
(* Goal: not (Col O C D) *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
intro.
(* Goal: False *)
rewrite H4 in H6.
basic_simpl;
(* Goal: False *)
intuition.
Qed.

Lemma free_points_ratio_elimination_4 : forall O U V A B C D : Point,
  parallel A B C D ->
  A<>B ->
  C<>D ->
  S O U V <> 0 ->
  S V C D <> 0 ->
  A**B / C**D = (S O V C * S O U B - S O V C * S O U A + S O U C * S O V A -
 S O U C * S O V B + S O V U * S O V A - S O V U * S O V B) /
(S O V C * S O U D + S O V C * S O V U - S O U C * S O V D -
 S O V D * S O V U).
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) *)
assert (S O V U <> 0).
(* Goal: False *)
intro; assert (Col O U V) by auto with Geom;intuition.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) *)
rewrite (free_points_ratio_elimination_3 O V U A B C D) by auto.
(* Goal: @eq F (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O V C) (S O U B)) (Fmult (S O V C) (S O U A))) (Fmult (S O U C) (S O V A))) (Fmult (S O U C) (S O V B))) (Fmult (S O V U) (S O V A))) (Fmult (S O V U) (S O V B))) (Fminus (Fminus (Fplus (Fmult (S O V C) (S O U D)) (Fmult (S O V C) (S O V U))) (Fmult (S O U C) (S O V D))) (Fmult (S O V D) (S O V U)))) *)
reflexivity.
Qed.

Lemma free_points_ratio_elimination_5 : forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col A C D ->
  A**B / C**D = (S O U C * S O V A - S O U C * S O V B - S O V A * S O U B +
 S O V B * S O U A - S O V C * S O U A + S O V C * S O U B) /
(S O U C * S O V A - S O U C * S O V D - S O V A * S O U D -
 S O V C * S O U A + S O V C * S O U D + S O U A * S O V D) .
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
rewrite (l2_15 A B C D) by auto with Geom.
(* Goal: @eq F (Fdiv (S C A B) (S A D C)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
assert (~ Col A D C) by auto with Geom.
(* Goal: @eq F (Fdiv (S C A B) (S A D C)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
unfold Col in H3.
(* Goal: @eq F (Fdiv (S C A B) (S A D C)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
rewrite (free_points_area_elimination O U V C A B) in * by assumption.
(* Goal: @eq F (Fdiv (Fdiv (Det3 (S O U C) (S O V C) F1 (S O U A) (S O V A) F1 (S O U B) (S O V B) F1) (S O U V)) (S A D C)) (Fdiv (Fplus (Fminus (Fplus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V B))) (Fmult (S O V A) (S O U B))) (Fmult (S O V B) (S O U A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fplus (Fplus (Fminus (Fminus (Fminus (Fmult (S O U C) (S O V A)) (Fmult (S O U C) (S O V D))) (Fmult (S O V A) (S O U D))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U D))) (Fmult (S O U A) (S O V D)))) *)
rewrite (free_points_area_elimination O U V A D C) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: and (not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0)) (not (@eq F (S O U V) F0)) *)
split;auto.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
replace (S O U A * S O V D - S O U A * S O V C - S O V A * S O U D +
      S O V A * S O U C + S O U D * S O V C - S O V D * S O U C)
   with (S O U C * S O V A - S O U C * S O V D - S O V A * S O U D - S O V C * S O U A +
S O V C * S O U D + S O U A * S O V D) in * by ring.
(* Goal: not (@eq F (Fminus (Fopp (Fmult xc (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)))) (Fopp (Fmult (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) xd))) F0) *)
intro Hx; rewrite Hx in *.
(* Goal: False *)
replace (0 / S O U V) with 0 in * by (field;auto).
(* Goal: False *)
intuition.
Qed.

(*
set (X_C := S O U C).
set (X_A := S O U A).
set (X_B := S O U B).
set (X_D := S O U D).
set (Y_C := S O V C).
set (Y_A := S O V A).
set (Y_B := S O V B).
set (Y_D := S O V D).
*)

Lemma free_points_ratio_elimination_6 : forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col O A C ->
  Col A C D ->
  A**B / C**D = (S O U A * S O V B - S O V A * S O U B) /
(S O U C * S O V D - S O V C * S O U D).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
assert (~ Col O C D).
(* Goal: not (Col O C D) *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
  intro.

(* Goal: False *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
  assert (Col C A O).
(* Goal: Col C A O *)
(* Goal: False *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
    apply (col_trans_1 C D A O );auto with Geom.
(* Goal: False *)
    intuition.

(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
assert (Col B C D).
(* Goal: Col B C D *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
  cut (Col C D B).
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
  auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
  apply (par_col_col_1 C D A B); auto with Geom.
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
rewrite <- (l2_7 C D A B O);auto.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
unfold Col in H4.
(* Goal: @eq F (Fdiv (S O A B) (S O C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
rewrite (free_points_area_elimination O U V O A B) in * by assumption.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
rewrite (free_points_area_elimination O U V O C D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: and (not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0)) (not (@eq F (S O U V) F0)) *)
split;auto.
(* Goal: not (@eq F (Fminus (Fopp (Fmult xc (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)))) (Fopp (Fmult (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) xd))) F0) *)
intro Hx; rewrite Hx in *.
(* Goal: False *)
replace (0 / S O U V) with 0 in * by (field;auto).
(* Goal: False *)
intuition.
Qed.

Lemma free_points_ratio_elimination_6_non_zero_denom: forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col O A C ->
  Col A C D ->
  S O U C * S O V D - S O V C * S O U D <> 0.
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
assert (~ Col O C D).
(* Goal: not (Col O C D) *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
  intro.

(* Goal: False *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
  assert (Col C A O).
(* Goal: Col C A O *)
(* Goal: False *)
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
    apply (col_trans_1 C D A O );auto with Geom.
(* Goal: False *)
    intuition.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
unfold Col in H4.
(* Goal: not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0) *)
rewrite (free_points_area_elimination O U V O C D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: not (@eq F (Fminus (Fopp (Fmult xc (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)))) (Fopp (Fmult (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) xd))) F0) *)
intro Hx; rewrite Hx in *.
(* Goal: False *)
replace (0 / S O U V) with 0 in * by (field;auto).
(* Goal: False *)
intuition.
Qed.


Lemma free_points_ratio_elimination_7 : forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col U A C ->
  Col A C D ->
  A**B / C**D = 
 (S O U V * (S O U B - S O U A) - S O U A * S O V B + S O U B * S O V A) /
 (S O U V * (S O U D - S O U C) - S O U C * S O V D + S O U D * S O V C).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.

(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
rewrite (free_points_ratio_elimination_6 U O V A B C D) by auto with Geom.
assert (S U O C * S U V D - S U V C * S U O D <> 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).

(* Goal: @eq F (Fdiv (Fminus (Fmult (S U O A) (S U V B)) (Fmult (S U V A) (S U O B))) (Fminus (Fmult (S U O C) (S U V D)) (Fmult (S U V C) (S U O D)))) (Fdiv (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U B) (S O U A))) (Fmult (S O U A) (S O V B))) (Fmult (S O U B) (S O V A))) (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C)))) *)
rewrite (free_points_area_elimination O U V U V A) in * by assumption.
(* Goal: @eq F (Fdiv (Fminus (Fmult (S U O A) (S U V B)) (Fmult (Fdiv (Det3 (S O U U) (S O V U) F1 (S O U V) (S O V V) F1 (S O U A) (S O V A) F1) (S O U V)) (S U O B))) (Fminus (Fmult (S U O C) (S U V D)) (Fmult (S U V C) (S U O D)))) (Fdiv (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U B) (S O U A))) (Fmult (S O U A) (S O V B))) (Fmult (S O U B) (S O V A))) (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C)))) *)
rewrite (free_points_area_elimination O U V U V B) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
rewrite (free_points_area_elimination O U V U V C) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
rewrite (free_points_area_elimination O U V U V D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
replace (S O V U) with (- S O U V) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O A) with (- S O U A) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O B) with (- S O U B) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O C) with (- S O U C) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O D) with (- S O U D) in * by auto with Geom.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.

(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xc := S O U C) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xa := S O U A) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xb := S O U B) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xd := S O U D) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd (S O V C))) F0) *)
set (yc := S O V C) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (ya := S O V A) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (yb := S O V B) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (yd := S O V D) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc)) F0) *)
set (X := S O U V) in *.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: and (not (@eq F (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D))) F0)) (not (@eq F (S O U V) F0)) *)
repeat split;auto.
replace ((0 - - (X * X) - X * xd + X * yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X * X) - X * xc + X * yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc * (X - xd + yd)) - - ((X - xc + yc) * xd))
  with (X * (xd - xc) - xc * yd + xd * yc) in H4 by ring.
(* Goal: not (@eq F (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc)) F0) *)
auto.
replace (- (xc * ((0 - - (X * X) - X * xd + X * yd) / X)) -
     - ((0 - - (X * X) - X * xc + X * yc) / X * xd))
  with ((- (xc * (- - (X * X) - X * xd + X * yd)) -
- ((- - (X * X) - X * xc + X * yc) * xd)) / X) in H4
     by (field;auto).
(* Goal: not (@eq F (Fminus (Fopp (Fmult xc (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)))) (Fopp (Fmult (Fplus (Fminus (Fopp (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) xd))) F0) *)
intro Hx; rewrite Hx in *.
(* Goal: False *)
replace (0 / X) with 0 in * by (field;auto).
(* Goal: False *)
intuition.
Qed.

Lemma free_points_ratio_elimination_7_non_zero_denom : 
  forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col U A C ->
  Col A C D ->
  (S O U V * (S O U D - S O U C) - S O U C * S O V D + S O U D * S O V C) <> 0.
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
assert (S U O C * S U V D - S U V C * S U O D <> 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
rewrite (free_points_area_elimination O U V U V C) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
rewrite (free_points_area_elimination O U V U V D) in * by assumption.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
unfold Det3 in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
replace (S O V U) with (- S O U V) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O A) with (- S O U A) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O B) with (- S O U B) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O C) with (- S O U C) in * by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S U O D) with (- S O U D) in * by auto with Geom.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
basic_simpl.

(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xc := S O U C) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xa := S O U A) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xb := S O U B) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) xc)) (Fmult xc (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
set (xd := S O U D) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd (S O V C))) F0) *)
set (yc := S O V C) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (ya := S O V A) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (yb := S O V B) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc (S O V D))) (Fmult xd yc)) F0) *)
set (yd := S O V D) in *.
(* Goal: not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc)) F0) *)
set (X := S O U V) in *.
replace ((0 - - (X * X) - X * xd + X * yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X * X) - X * xc + X * yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc * (X - xd + yd)) - - ((X - xc + yc) * xd))
  with (X * (xd - xc) - xc * yd + xd * yc) in H4 by ring.
(* Goal: not (@eq F (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc)) F0) *)
auto.
Qed.

Lemma free_points_ratio_elimination_8 : forall O U V A B C D: Point,
  parallel A B C D ->
  C<>D ->
  ~ Col O U V ->
  ~ Col V A C ->
  Col A C D ->
  A**B / C**D = 
    ( S O U V * (S O V B - S O V A) + S O V A * S O U B - S O V B * S O U A) /
    ( S O U V * (S O V D - S O V C) + S O V C * S O U D - S O V D * S O U C).
Proof.
(* Goal: forall (O U V A B C D : Point) (_ : parallel A B C D) (_ : not (@eq Point C D)) (_ : not (Col O U V)) (_ : not (Col U A C)) (_ : Col A C D), not (@eq F (Fplus (Fminus (Fmult (S O U V) (Fminus (S O U D) (S O U C))) (Fmult (S O U C) (S O V D))) (Fmult (S O U D) (S O V C))) F0) *)
intros.
(*
set (X_C := S O U C).
set (X_A := S O U A).
set (X_B := S O U B).
set (X_D := S O U D).
set (Y_C := S O V C).
set (Y_A := S O V A).
set (Y_B := S O V B).
set (Y_D := S O V D).
*)
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
rewrite (free_points_ratio_elimination_7 O V U A B C D) by auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S O V U) with (- S O U V) by auto with Geom.
(* Goal: @eq F (Fdiv (Fminus (Fopp (Fmult xa (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xb)) (Fmult X yb)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xa)) (Fmult X ya)) X) xb))) (Fminus (Fopp (Fmult xc (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xd)) (Fmult X yd)) X))) (Fopp (Fmult (Fdiv (Fplus (Fminus (Fminus F0 (Fopp (Fmult X X))) (Fmult X xc)) (Fmult X yc)) X) xd)))) (Fdiv (Fplus (Fminus (Fmult X (Fminus xb xa)) (Fmult xa yb)) (Fmult xb ya)) (Fplus (Fminus (Fmult X (Fminus xd xc)) (Fmult xc yd)) (Fmult xd yc))) *)
field.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (- S O U V) with (S O V U) by auto with Geom.
(* Goal: and (@eq F (Fdiv (S U C D') (Fplus (Fplus (S U C O) (S U O D)) (S O C D))) (Fdiv (Fminus (S U A B) (S C A B)) (Fminus (Fplus (S O C D) (S O U C)) (S O U D)))) (not (@eq F (Fminus (Fplus (S O C D) (S O U C)) (S O U D)) F0)) *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fplus (Fminus (Fplus (Fminus (Fmult (S O U C) (S O V B)) (Fmult (S O U C) (S O V A))) (Fmult (S O V C) (S O U A))) (Fmult (S O V C) (S O U B))) (Fmult (S O U V) (S O U A))) (Fmult (S O U V) (S O U B))) (Fminus (Fminus (Fplus (Fmult (S O U C) (S O V D)) (Fmult (S O U C) (S O U V))) (Fmult (S O V C) (S O U D))) (Fmult (S O U D) (S O U V)))) *)
split.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
replace (S O U V) with (- S O V U) by auto with Geom.
replace (- S O V U * (S O V D - S O V C) + S O V C * S O U D - S O V D * S O U C)
with    (- (S O V U * (S O V D - S O V C) - S O V C * S O U D + S O V D * S O U C))
 by ring.
Lemma aux: forall x, x<>0 -> -x<>0.
Proof.
auto with field_hints.
Qed. 
apply aux.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
(* Goal: forall _ : Col C D B, Col B C D *)
(* Goal: Col C D B *)
(* Goal: @eq F (Fdiv (DSeg A B) (DSeg C D)) (Fdiv (Fminus (Fmult (S O U A) (S O V B)) (Fmult (S O V A) (S O U B))) (Fminus (Fmult (S O U C) (S O V D)) (Fmult (S O V C) (S O U D)))) *)
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
Qed.

