(***************************************************************************)
(* 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 area_method.

(* A small lemma to check that centroid is really at the 
intersection of medians. *)

Lemma centroid_check : forall A B C G A',
 is_centroid G A B C ->
 is_midpoint A' B C ->
 Col A G A'.
Proof.
(* Goal: forall (A B C G P Q : Point) (_ : is_centroid G A B C) (_ : on_inter_line_parallel P G A B B C) (_ : on_inter_line_parallel Q G A C B C) (_ : not (@eq Point G Q)) (_ : not (@eq Point G P)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)), @eq F (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S4 P Q C B)) (Fmult (Fplus (Fplus (Fplus F1 F1) (Fplus F1 F1)) F1) (S A Q P)) *)
area_method.
Qed.

Lemma euler_line : forall A B C H O G,
  is_circumcenter O A B C ->
  is_orthocenter H A B C ->
  is_centroid G A B C ->
  Col O G H.
Proof.
(* Goal: forall (A B C G P Q : Point) (_ : is_centroid G A B C) (_ : on_inter_line_parallel P G A B B C) (_ : on_inter_line_parallel Q G A C B C) (_ : not (@eq Point G Q)) (_ : not (@eq Point G P)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)), @eq F (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S4 P Q C B)) (Fmult (Fplus (Fplus (Fplus F1 F1) (Fplus F1 F1)) F1) (S A Q P)) *)
area_method.
Qed.

Lemma centroid_midpoint_centroid : forall A B C G A' B' C' G' X,
 is_centroid G A B C ->
 is_midpoint A' B C ->
 is_midpoint B' A C ->
 is_midpoint C' A B ->
 is_centroid G' A' B' C' ->
 1+2<>0 ->
 Col G G' X.
Proof.
(* Goal: forall (A B C G P Q : Point) (_ : is_centroid G A B C) (_ : on_inter_line_parallel P G A B B C) (_ : on_inter_line_parallel Q G A C B C) (_ : not (@eq Point G Q)) (_ : not (@eq Point G P)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)), @eq F (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S4 P Q C B)) (Fmult (Fplus (Fplus (Fplus F1 F1) (Fplus F1 F1)) F1) (S A Q P)) *)
area_method.
Qed.

Lemma centroid_midpoint_centroid_2 : forall A B C G A' B' C' G',
 is_centroid G A B C ->
 is_midpoint A' B C ->
 is_midpoint B' A C ->
 is_midpoint C' A B ->
 is_centroid G' A' B' C' ->
 1+2<>0 ->
 Py G G' G = 0.
Proof.
(* Goal: forall (A B C G M N : Point) (_ : is_centroid G A B C) (_ : on_line M A B) (_ : inter_ll N G M A C) (_ : parallel M B A M) (_ : not (@eq Point A M)) (_ : not (@eq Point A N)) (_ : parallel N C A N) (_ : not (@eq Point B M)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)) (_ : not (@eq F (Fplus (Fplus F1 F1) F1) F0)), @eq F (Fplus (Fdiv (DSeg M B) (DSeg A M)) (Fdiv (DSeg N C) (DSeg A N))) F1 *)
geoInit.
(* Goal: @eq F (Py G G' G) F0 *)
eliminate G'.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A' G A')) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A' G B'))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A' G C')))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B' G A')) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B' G B'))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B' G C'))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G A')) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G B'))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G C'))))) F0 *)
eliminate A'.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B' G B))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B' G B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B' G B'))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B' G C'))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G B'))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G C'))))) F0 *)
eliminate B'.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C' G A))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C' G C'))))) F0 *)
eliminate C'.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A)))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G C)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G A))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py C G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G A))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py B G A)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G B)) (Fmult (Fdiv F1 (Fplus F1 F1)) (Py A G A))))))))) F0 *)
eliminate G.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B C)))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B C)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B C)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A C))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A C))))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B C)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A C))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A B C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B A)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C B C)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B C A)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py A C B)) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A B A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py A C A))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Py B C B)))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py B A C)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A B)) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Py C A C))))))))))))) F0 *)
unfold_Py.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C B)) (DSeg C B))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C)))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C B)) (DSeg C B))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B A))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C A)) (DSeg C A)))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B A))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C A)) (DSeg C A)))))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C B)) (DSeg C B))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B A))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C A)) (DSeg C A)))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C B) (DSeg C B)) (Fmult (DSeg B A) (DSeg B A))) (Fmult (DSeg C A) (DSeg C A)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C B)) (DSeg C B))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (DSeg C A) (DSeg C A))) (Fmult (DSeg B A) (DSeg B A)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (DSeg C B) (DSeg C B))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B A))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B A) (DSeg B A)) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg C A) (DSeg C A)) (Fmult (DSeg A B) (DSeg A B))) (Fmult (DSeg C B) (DSeg C B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg C A)) (DSeg C A)))))))))))))) F0 *)
uniformize_dir_seg.
(* Goal: @eq F (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg B C))) (Fopp (DSeg B C)))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C)))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg B C))) (Fopp (DSeg B C)))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A B))) (Fopp (DSeg A B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A C))) (Fopp (DSeg A C))))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A B))) (Fopp (DSeg A B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A C))) (Fopp (DSeg A C))))))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg B C))) (Fopp (DSeg B C)))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A B))) (Fopp (DSeg A B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A C))) (Fopp (DSeg A C))))))))))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B)))) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg B C))) (Fopp (DSeg B C)))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg B C) (DSeg B C)) (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C)))) (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus F1 F1)) (Fminus (Fminus (Fminus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (DSeg A C) (DSeg A C)) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C)))) (Fmult (DSeg A B) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg A C)) (DSeg A C)))) (Fmult (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fdiv F1 (Fplus (Fplus F1 F1) F1))) (Fmult (Fmult (Fplus F1 F1) (DSeg B C)) (DSeg B C))))) (Fmult (Fdiv F1 (Fplus F1 F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A B))) (Fopp (DSeg A B)))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A B)) (Fopp (DSeg A B))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (DSeg B C) (DSeg B C)))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fplus (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fminus (Fplus (Fmult (Fopp (DSeg A C)) (Fopp (DSeg A C))) (Fmult (DSeg A B) (DSeg A B))) (Fmult (Fopp (DSeg B C)) (Fopp (DSeg B C))))) (Fmult (Fdiv F1 (Fplus (Fplus F1 F1) F1)) (Fmult (Fmult (Fplus F1 F1) (Fopp (DSeg A C))) (Fopp (DSeg A C))))))))))))))) F0 *)
field_and_conclude.
Qed.

Lemma l6_44 : forall A B C G P Q,
 is_centroid G A B C ->
 on_inter_line_parallel P G A B B C  ->
 on_inter_line_parallel Q G A C B C  ->
 G<>Q -> G<>P -> 1+2 <> 0 ->
 2*2*S4 P Q C B = (2+2+1)* S A Q P.
Proof.
(* Goal: forall (A B C G P Q : Point) (_ : is_centroid G A B C) (_ : on_inter_line_parallel P G A B B C) (_ : on_inter_line_parallel Q G A C B C) (_ : not (@eq Point G Q)) (_ : not (@eq Point G P)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)), @eq F (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S4 P Q C B)) (Fmult (Fplus (Fplus (Fplus F1 F1) (Fplus F1 F1)) F1) (S A Q P)) *)
area_method.
Qed.

Lemma l6_47 : forall A B C G M N,
 is_centroid G A B C ->
 on_line M A B ->
 inter_ll N G M A C ->
 parallel M B A M -> A<>M -> A<>N ->
 parallel N C A N -> B<>M ->
 1+2<> 0 -> 2+1 <> 0 ->
 M**B/A**M + N**C/A**N = 1.
Proof.
(* Goal: forall (A B C G M N : Point) (_ : is_centroid G A B C) (_ : on_line M A B) (_ : inter_ll N G M A C) (_ : parallel M B A M) (_ : not (@eq Point A M)) (_ : not (@eq Point A N)) (_ : parallel N C A N) (_ : not (@eq Point B M)) (_ : not (@eq F (Fplus F1 (Fplus F1 F1)) F0)) (_ : not (@eq F (Fplus (Fplus F1 F1) F1) F0)), @eq F (Fplus (Fdiv (DSeg M B) (DSeg A M)) (Fdiv (DSeg N C) (DSeg A N))) F1 *)
geoInit.
(* Goal: @eq F (Fplus (Fdiv (DSeg M B) (DSeg A M)) (Fdiv (DSeg N C) (DSeg A N))) F1 *)
am_before_field.
(* Goal: @eq F (Fminus (Fopp (Fmult (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f) (Finv f))) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus (Fopp (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f)) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
field;solve_conds.
(* Goal: not (@eq F (Fopp (Fmult f (S C A B))) F0) *)
(* Goal: @eq F (Fminus (Fopp (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f)) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
intro.
(* Goal: False *)
(* Goal: @eq F (Fminus (Fopp (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f)) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
replace (- (f * (/ (2 + 1) * S C A B))) with (- (f * S C A B) / (2+1)) in H7 by (field;solve_conds).
(* Goal: False *)
(* Goal: @eq F (Fminus (Fopp (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f)) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
rewrite H13 in H7.
(* Goal: False *)
(* Goal: @eq F (Fminus (Fopp (Fplus (Fopp (Fmult (DSeg A B) (Finv (DSeg A B)))) f)) (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
replace (0 / (2 + 1)) with (0) in H7 by (field;solve_conds).
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
intuition.
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
intuition.
(* Goal: @eq F (Fminus F0 (Fmult (Fminus (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))) (Fmult (Fminus F1 f) (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B)))) (Finv (Fopp (Fmult f (Fmult (Finv (Fplus (Fplus F1 F1) F1)) (S C A B))))))) F1 *)
intuition.
Qed.
