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

Require Export basic_geometric_facts.

Theorem common_point_not_par_aux :
 forall A B C D Y : Point,
 Col Y A B ->
 Col Y C D -> 
 A <> B -> 
 C <> D -> 
 ~ Col D A B -> 
 ~ Col Y A C -> 
 ~ parallel A B C D.
Proof with Geometry. 
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
assert (D <> Y).
unfold not;intro;subst D...
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
assert (C ** Y / D ** Y = S C A B / S D A B)...
assert (S C A B = S D A B).
unfold parallel in H6.
unfold S4 in H6.
assert (S C A B = - S A C B)...
rewrite H8.
RewriteVar (S A C B) H6.
ring_simplify.
(* Goal: not (parallelogram A B D D) *)
Geometry.
rewrite H8 in H7.
assert (C ** Y = D ** Y).
RewriteVar (C ** Y) H7.
field...
(* Goal: not (parallelogram A B D D) *)
Geometry.
assert (C = D).
assert (C ** D + D ** Y = C ** Y)...
rewrite <- H10 in H9.
assert (C ** D = 0)...
RewriteVar (C ** D) H9...
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Lemma col_par_1 : forall A B C,
 Col A B C -> parallel A B B C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B D *)
unfold parallel, S4, Col in *.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
rewrite H.
(* Goal: @eq F (Fplus (S B B A) (S B A C)) F0 *)
basic_simpl.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
Qed.

Lemma col_par_2 : forall A B C,
 Col A B C -> parallel A B C B.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B D *)
unfold parallel, S4, Col in *.
(* Goal: @eq F (Fplus (S B B A) (S B A C)) F0 *)
basic_simpl.
(* Goal: @eq F (S A B D) F0 *)
uniformize_signed_areas.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
rewrite H.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
Qed.

Lemma col_par_3 : forall A B C,
 Col A B C -> parallel B A C B.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B D *)
unfold parallel, S4, Col in *.
(* Goal: @eq F (Fplus (S B B A) (S B A C)) F0 *)
basic_simpl.
(* Goal: @eq F (S A B D) F0 *)
uniformize_signed_areas.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
rewrite H.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
Qed.

Lemma col_par_4 : forall A B C,
 Col A B C -> parallel B A B C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B D *)
unfold parallel, S4, Col in *.
(* Goal: @eq F (Fplus (S B B A) (S B A C)) F0 *)
basic_simpl.
(* Goal: @eq F (S A B D) F0 *)
uniformize_signed_areas.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
rewrite H.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
Qed.

Hint Resolve col_par_1 col_par_2 col_par_3 col_par_4 : Geom. 

Lemma par_col_col_1 : forall A B C D, 
 parallel A B C D ->
 Col A B C -> 
 Col A B D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B D *)
unfold parallel,S4,Col in *.
(* Goal: @eq F (S A B D) F0 *)
uniformize_signed_areas.
(* Goal: @eq F (S A B D) F0 *)
RewriteVar (S A B D) H.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
replace (- (1) * S A C B) with (- S A C B) by ring.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
Qed.

Lemma par_col_col_2 : forall A B C D, 
 parallel A B C D ->
 Col A B D -> 
 Col A B C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A B C *)
assert (parallel A B D C).
(* Goal: not (parallelogram A B D D) *)
Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
eapply par_col_col_1;eauto.
Qed.

Lemma par_col_col_3 : forall A B C D, 
 parallel A B C D ->
 Col A C D -> 
 Col B C D.
Proof with Geometry.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
cut (Col C D B).
(* Goal: not (parallelogram A B D D) *)
Geometry.
assert (parallel C D A B).
(* Goal: not (parallelogram A B D D) *)
Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
eapply par_col_col_1;eauto...
Qed.

Lemma par_col_col_4 : forall A B C D, 
 parallel A B C D ->
 Col B C D -> 
 Col A C D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: Col A C D *)
cut (Col C D A).
(* Goal: not (parallelogram A B D D) *)
Geometry.
(* Goal: Col C D A *)
assert (parallel C D B A).
(* Goal: not (parallelogram A B D D) *)
Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
eapply par_col_col_1;eauto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Theorem common_point_not_par :
 forall A B C D Y : Point,
 Col Y A B -> 
 Col Y C D -> 
 A <> B -> 
 C <> D ->
 ~ Col Y A C -> 
 ~ parallel A B C D. 
Proof with Geometry.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
cases_col D A B.
unfold parallel, S4 in |- *.
cut (Y = D).
intro.
assert (S A B D = S D A B)...
rewrite H6.
rewrite H4.
unfold not in |- *.
intro.
NormalizeRing H7.
clear H H0.
rewrite H5 in H3.
clear H5.
clear H6.
assert (Col A B D)...
assert (Col A B C)...
assert (Col A D C); eauto with Geom.
assert (Col A B Y)...
assert (Col A B D)...
assert (Col A Y D); eauto with Geom.
assert (A <> Y); eauto with Geom.
cases_equality Y D.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
assert (Col Y D A)...
assert (Col Y D C)...
assert (Col Y A C); eauto with Geom.
(* Goal: False *)
intuition.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
eapply common_point_not_par_aux; apply H || auto.
Qed.

Definition parallelogram (A B C D : Point) : Prop :=
  parallel A B C D /\ parallel B C A D /\ ~ Col A B C.


Theorem l1_24 :
 forall A B C D O : Point,
 parallelogram A B C D -> 
 Col A C O -> 
 Col B D O -> 
 A ** O = O ** C.
Proof with Geometry.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
unfold parallelogram in H.
DecompAndAll.
unfold parallel,S4 in *.
assert (S A B D = S A B C).
RewriteVar (S A B D) H2...
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
replace (-(1) * S A C B) with (- S A C B) by ring...
assert (S B C D = S B C A).
RewriteVar (S B C D) H4...
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
replace (-(1) * S B A C) with (- S B A C) by ring...
assert (S C B D = - S B C A).
rewrite <- H3...
assert (~ Col C B D).
unfold not in |- *; intro.
rewrite H7 in H6...
assert (A ** O / C ** O = S A B D / S C B D).
apply co_side...
unfold not in |- *; intro.
subst O...
rewrite H in H8...
rewrite H6 in H8...
assert (S A B C = S B C A)...
rewrite H9 in H8...
assert (C ** O = - O ** C)...
rewrite H10 in H8...
RewriteVar (A ** O) H8...
field...
rewrite <- H10.
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (O <> C).
unfold not; intro;subst O...
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.


Theorem diago_par_intersect :
 forall A B C D : Point, 
 parallelogram A B C D -> 
 ~ parallel A C B D.
Proof with Geometry.
(* Goal: forall (A B C D : Point) (_ : parallelogram A B C D), not (Col A C D) *)
unfold parallelogram,parallel, S4 in |- *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
DecompAndAll.
assert (S A C D = S A C B + S A B D + S B C D)...
RewriteVar (S A C B) H0.
RewriteVar (S B C D) H2.
NormalizeRing H.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
rewrite H.
replace (S B A C) with (- S A B C)...
ring_simplify (S A B C + - - S A B C)...
Qed.

Theorem para_not_col_1 :
 forall A B C D : Point, 
 parallelogram A B C D -> 
 ~ Col A B D. 
Proof.
(* Goal: forall (A B C D : Point) (_ : parallelogram A B C D), not (Col A C D) *)
unfold parallelogram, parallel, S4 in |- *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
unfold not in |- *; intro.
(* Goal: False *)
rewrite H1 in H0.
(* Goal: False *)
NormalizeRing H0.
(* Goal: not (parallelogram A B D D) *)
assert (Col A C B); Geometry.
Qed.

Hint Resolve para_not_col_1: Geom.

Theorem para_not_col_2 :
 forall A B C D : Point, parallelogram A B C D -> ~ Col B C D. 
Proof.
(* Goal: forall (A B C D : Point) (_ : parallelogram A B C D), not (Col A C D) *)
unfold parallelogram, parallel, S4 in |- *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
unfold not in |- *; intro.
(* Goal: @eq F (Fdiv (DSeg O C) (DSeg A C)) (Fdiv F1 (Fplus F1 F1)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
rewrite H1 in H2.
(* Goal: False *)
NormalizeRing H2.
(* Goal: not (parallelogram A B D D) *)
assert (Col B A C); Geometry.
Qed.

Hint Resolve para_not_col_2: Geom.

Theorem para_not_col_3 :
 forall A B C D : Point, parallelogram A B C D -> ~ Col A C D. 
Proof.
(* Goal: forall (A B C D : Point) (_ : parallelogram A B C D), not (Col A C D) *)
unfold parallelogram, parallel,S4 in |- *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
unfold not in |- *; intro.
(* Goal: not (parallelogram A B D D) *)
assert (S A C D = S A C B + S A B D + S B C D); Geometry.
(* Goal: False *)
rewrite H1 in H4.
(* Goal: False *)
rewrite H0 in H4.
(* Goal: False *)
NormalizeRing H4.
(* Goal: not (parallelogram A B D D) *)
assert (Col B C D); Geometry.
(* Goal: False *)
assert (parallelogram A B C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold parallelogram in |- *; auto.
(* Goal: False *)
assert (~ Col B C D); eauto with Geom.
Qed.

Hint Resolve para_not_col_3: Geom.


Theorem para_1 : forall A B C D : Point, 
  parallelogram A B C D -> parallelogram A D C B.
Proof.
(* Goal: forall (A B C D : Point) (_ : parallelogram A B C D), parallelogram A D C B *)
unfold parallelogram in |- *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
(* Goal: not (parallelogram A B D D) *)
repeat split; Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (parallelogram A B C D); unfold parallelogram in |- *; auto.
(* Goal: not (Col A D C) *)
assert (~ Col A C D); eauto with Geom.
Qed.

Hint Resolve para_1: Geom.


Theorem para_2 : forall A B C D : Point, 
  parallelogram A B C D -> parallelogram B A D C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: parallelogram B A D C *)
assert (~Col A B D).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: parallelogram C B A D *)
unfold parallelogram in *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
(* Goal: not (parallelogram A B D D) *)
repeat split; Geometry.
Qed.

Hint Resolve para_2: Geom.

Theorem para_3 : forall A B C D : Point, 
  parallelogram A B C D -> parallelogram D C B A.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: parallelogram C B A D *)
assert (~Col D C B).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: parallelogram C B A D *)
unfold parallelogram in *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
(* Goal: not (parallelogram A B D D) *)
repeat split; Geometry.
Qed.

Hint Resolve para_3: Geom.

Theorem para_4 : forall A B C D : Point, 
  parallelogram A B C D -> parallelogram C B A D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: parallelogram C B A D *)
assert (~Col D C B).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: parallelogram C B A D *)
unfold parallelogram in *.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: and (parallel C B A D) (and (parallel B A C D) (not (Col C B A))) *)
decompose [and] H.
(* Goal: not (parallelogram A B D D) *)
repeat split; Geometry.
Qed.

Hint Resolve para_4: Geom.


Theorem not_para_eq_1 : forall A B C, ~ parallelogram A A B C.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col A A C).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.

Theorem not_para_eq_2 : forall A B C, ~ parallelogram A B C C.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col B C C).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.


Theorem not_para_eq_3 : forall A B C, ~ parallelogram A B C A.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col A B A).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.

Theorem not_para_eq_4 : forall A B C, ~ parallelogram A B B C.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col A B B).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.

Theorem not_para_eq_5 : forall A B C, ~ parallelogram A B A C.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col A A C).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.


Theorem not_para_eq_6 : forall A B C, ~ parallelogram A B C B.
Proof.
(* Goal: forall A B C : Point, not (parallelogram A B C B) *)
intuition idtac.
(* Goal: False *)
assert (~ Col B C B).
(* Goal: not (Col B C B) *)
(* Goal: False *)
eauto with Geom.
(* Goal: False *)
intuition.
Qed.


Hint Resolve not_para_eq_1 not_para_eq_2 not_para_eq_3 
not_para_eq_4 not_para_eq_5 not_para_eq_6 : Geom.


Theorem para_not_eq_1 : forall A B C D, 
  parallelogram A B C D -> A<>B.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst A.
(* Goal: False *)
cut (~parallelogram B B C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Theorem para_not_eq_2 : forall A B C D, 
  parallelogram A B C D -> A<>C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst A.
(* Goal: False *)
cut (~parallelogram C B C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Theorem para_not_eq_3 : forall A B C D, 
  parallelogram A B C D -> A<>D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst A.
(* Goal: False *)
cut (~parallelogram D B C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Theorem para_not_eq_4 : forall A B C D, 
  parallelogram A B C D -> B<>C.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst B.
(* Goal: False *)
cut (~parallelogram A C C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.


Theorem para_not_eq_5 : forall A B C D, 
  parallelogram A B C D -> B<>D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst B.
(* Goal: False *)
cut (~parallelogram A D C D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Theorem para_not_eq_6 : forall A B C D, 
  parallelogram A B C D -> C<>D.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
(* Goal: False *)
subst C.
(* Goal: False *)
cut (~parallelogram A B D D).
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
Qed.

Hint Resolve para_not_eq_1 para_not_eq_2 para_not_eq_3
 para_not_eq_4 para_not_eq_5 para_not_eq_6 : Geom.


Theorem mid_point_equation :
 forall A C O P Q : Point,
 Col O A C -> A <> C -> A ** O = O ** C -> 
 S A P Q + S C P Q = 2 * S O P Q.
Proof.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
assert (T := l2_9 P Q A C O H0 H).
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
rewrite H1 in T.
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
rewrite T.
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (O ** C / A ** C = 1 / 2).
(* Goal: not (parallelogram A B D D) *)
assert (A ** O + O ** C = A ** C); Geometry.
(* Goal: @eq F (Fdiv (DSeg O C) (DSeg A C)) (Fdiv F1 (Fplus F1 F1)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
rewrite H1 in H2.
(* Goal: @eq F (Fdiv (DSeg O C) (DSeg A C)) (Fdiv F1 (Fplus F1 F1)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
rewrite <- H2.
(* Goal: @eq F (Fdiv (DSeg O C) (Fplus (DSeg O C) (DSeg O C))) (Fdiv F1 (Fplus F1 F1)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
field.
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (O ** C + O ** C = 2 * O ** C).
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (O <> C).
unfold not in |- *; intro.
(* Goal: not (parallelogram A B D D) *)
assert (O ** C = 0); Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
rewrite H5 in H1.
(* Goal: not (parallelogram A B D D) *)
assert (A = O); Geometry.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
assert (A = C).
(* Goal: @eq Point A C *)
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
congruence.
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
rewrite H3; Geometry.
(* Goal: not (parallelogram A B D D) *)
rewrite H2; field; Geometry.
Qed.




Theorem col_par_par :  forall A B C D D',  
 ~C=D -> 
 parallel A B C D -> 
 Col C D D' -> 
 parallel A B C D'.
Proof with Geometry.
(* Goal: forall (A C O P Q : Point) (_ : Col O A C) (_ : not (@eq Point A C)) (_ : @eq F (DSeg A O) (DSeg O C)), @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (S O P Q)) *)
intros.
cases_col A C D.
assert (Col C D B).
eapply par_col_col_1 with (C:=A)...
assert (Col C A B).
eapply col_trans_1 with (B:=D)...
assert (Col D A B).
eapply col_trans_1 with (B:=C)...
unfold parallel, S4 in *.
replace (S A C B) with (- S C A B).
rewrite H4.
ring_simplify.
assert (Col C A D').
eapply col_trans_1 with (B:=D)...
cases_equality A C.
(* Goal: False *)
subst A.
assert (Col C B D').
eapply col_trans_1 with (B:=D)...
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
assert (Col  A B D').
eapply col_trans_1 with (B:=C)...
(* Goal: False *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
auto.
(* Goal: not (parallelogram A B D D) *)
Geometry.
assert (~Col B C D).
(* Goal: not (@eq Point O C) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
unfold not;intro.
assert (Col C D A).
eapply par_col_col_1 with (C:=B)...
assert (Col A C D)...

assert (parallel A B C D)...
unfold parallel, S4 in H4.
unfold parallel,S4.

assert (C**D' / C**D = S A C D' / S A C D).
apply A6...
assert (C**D' / C**D = S B C D' / S B C D).
apply A6...
set (C ** D' / C ** D) in *.

RewriteVar (S A C B) H4.

replace (S A B D) with (S A B C + S A C D + S C B D).
(* Goal: not (parallelogram A B D D) *)
2:symmetry;Geometry.
replace (S A B D') with (S A B C + S A C D' + S C B D').
(* Goal: not (parallelogram A B D D) *)
2:symmetry;Geometry.
ring_simplify.
RewriteVar (S A C D') H5.
(* Goal: not (parallelogram A B D D) *)
2:Geometry.
replace (S C B D') with (- S B C D').
(* Goal: not (parallelogram A B D D) *)
2:Geometry.
RewriteVar (S B C D') H6.
(* Goal: not (parallelogram A B D D) *)
2:Geometry.
replace (S B C D) with (-S C B D).
(* Goal: not (parallelogram A B D D) *)
2:Geometry.
ring_simplify.
replace ( S A C D * f - S A C D + S C B D * f - S C B D) with
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
((S A C D + S C B D) * (f-1)) by ring.
replace (S A C D + S C B D) with 0.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.

symmetry.
assert (parallel  C D B A)...
unfold parallel,S4 in *.
RewriteVar (S C B D) H9.
(* Goal: @eq F (S A B D) F0 *)
uniformize_signed_areas.
(* Goal: @eq F (Fplus (DSeg O C) (DSeg O C)) (Fmult (Fplus F1 F1) (DSeg O C)) *)
(* Goal: and (not (@eq F (Fplus F1 F1) F0)) (not (@eq F (Fplus (DSeg O C) (DSeg O C)) F0)) *)
(* Goal: @eq F (Fplus (S A P Q) (S C P Q)) (Fmult (Fplus F1 F1) (Fplus (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S C P Q)) (Fmult (Fdiv (DSeg O C) (DSeg A C)) (S A P Q)))) *)
ring.
Qed.














