# Library AreaMethod.examples_2

Require Import area_method.

Lemma l3_43 : O A B X Y C D P Q R T r,
mratio C A B r
mratio D A B (0-r)
inter_ll P O A X Y
inter_ll Q O B X Y
inter_ll R O C X Y
inter_ll T O D X Y
parallel P R R Q
RQ
parallel T P T Q
TQ
PT
PR
¬ Col P X Y
harmonic P Q R T.
Proof.
area_method.
Qed.

Theorem Ceva :
A B C D E F G P : Point,
inter_ll D B C A P
inter_ll E A C B P
inter_ll F A B C P
F B
D C
E A
parallel A F F B
parallel B D D C
parallel C E E A
(A ** F / F ** B) × (B ** D / D ** C) × (C ** E / E ** A) = 1.
Proof.
area_method.
Qed.

Lemma l6_217 : A B C D E F G H,
is_midpoint E A B
is_midpoint F B C
is_midpoint G C D
is_midpoint H D A
parallel H E G F
GF
EH
¬ Col E D A
H**E / G**F = 1.
Proof.
area_method.
Qed.

Theorem Menelaus :
A B C X Y D E F : Point,
inter_ll D B C X Y
inter_ll E A C X Y
inter_ll F A B X Y
F B
D C
E A
parallel A F F B
parallel B D D C
parallel C E E A
(A ** F / F ** B) × (B ** D / D ** C) × (C ** E / E ** A) = - (1).
Proof.
area_method.
Qed.

Theorem Pascal :
A B C A' B' C' : Point, AC'
on_line C A B
on_parallel B' A B A'
on_inter_line_parallel C' A A' B' C A'
parallel B C' B' C.
Proof.
area_method.
Qed.

Theorem Desargues :
A B C X A' B' C' : Point, A' C' A' B'
on_line A' X A
on_inter_line_parallel B' A' X B A B
on_inter_line_parallel C' A' X C A C
parallel B C B' C'.
Proof.
area_method.
Qed.

Theorem ex1_6auto :
A B C D E F G P : Point,
inter_ll D B C A P
inter_ll E A C B P
inter_ll F A B C P
A D
B E
C F
parallel P D A D
parallel P E B E
parallel P F C F
P ** D / A ** D + P ** E / B ** E + P ** F / C ** F = 1.
Proof.
area_method.
Qed.

Theorem th2_41 :
A B C D P Q M : Point,
on_line C A P
on_inter_line_parallel D C B P A B
inter_ll Q A D B C
inter_ll M A B P Q
B M
parallel A M B M
CD
A ** M / B ** M = - (1).
Proof.
area_method.
Qed.

Theorem Prop51Hartsshorne :
A B C D E : Point,
is_midpoint D A B
is_midpoint E A C
parallel D E B C.
Proof.
area_method.
Qed.

Theorem is_midpoint_A :
A B C A' B' : Point,
is_midpoint A' B C
is_midpoint B' A C
parallel A' B' A B.
Proof.
area_method.
Qed.

Theorem Prop51Hartsshornebis :
A B C D E : Point,
¬ Col D A C
¬ Col A B C
is_midpoint D A B
is_midpoint E A C
parallel D E B C
B C
D ** E / B ** C = 1 / 2.
Proof.
area_method.
Qed.

Theorem th6_40_Centroid :
A B C E F O : Point,
is_midpoint F A B
is_midpoint E B C
inter_ll O A E C F
O E
parallel A O O E
A ** O / O ** E = 2.
Proof.
area_method.
Qed.

Theorem Prop54Hartsshorne :
A B C D E F G : Point,
is_midpoint D A B
is_midpoint E A C
is_midpoint F B C
inter_ll G E B C D
Col A G F.
Proof.
area_method.
Qed.

Theorem Exo55Hartsshorne :
A B C D I J K L,
is_midpoint I A B
is_midpoint J B C
is_midpoint K C D
is_midpoint L D A
parallel I J K L parallel I L J K.
Proof.
area_method.
Qed.

Theorem th6_42 :
A B C L M N P K : Point,
is_midpoint M A B
is_midpoint N A C
is_midpoint K B C
is_midpoint L A K
on_inter_parallel_parallel P A C M K B N
PA
(2 + 2) × S A K P = (1 + 2) × S A B C.
Proof.
am_before_field.
intuition.
field_and_conclude.
Qed.

Theorem th6_43 :
A B C F N K : Point,
is_midpoint F A B
is_midpoint N C F
inter_ll K B C A N
K C
parallel B K K C
B ** K / K ** C = 2.
Proof.
area_method.
Qed.

Theorem Conversemenelaus :
(A B C D E G : Point) (r1 r2 : F),
mratio D B C r1
mratio E C A r2
inter_ll G D E A B
G A
parallel B G G A
B ** G / G ** A = - r1 × r2.
Proof.
area_method.
Qed.

A B C D X Y A1 B1 C1 D1 : Point,
inter_ll A1 A B X Y
inter_ll B1 B C X Y
inter_ll C1 C D X Y
inter_ll D1 A D X Y
B A1
C B1
D C1
A D1
parallel A A1 B A1
parallel B B1 C B1
parallel C C1 D C1
parallel D D1 A D1
A ** A1 / B ** A1 × (B ** B1 / C ** B1 × (C ** C1 / D ** C1 × (D ** D1 / A ** D1))) =
1.
Proof.
area_method.
Qed.

(A B C D A1 B1 C1 D1 : Point) (r1 r2 : F),
mratio B1 B C r1
mratio C1 C D r2
inter_ll D1 D A B1 C1
inter_ll A1 A B B1 C1
A1 A
D1 A
parallel B A1 A1 A
parallel D D1 D1 A B ** A1 / A1 ** A = r1 × (r2 × (D ** D1 / D1 ** A)).
Proof.
area_method.
Qed.

Theorem th6_6 :
A B C L M N O : Point,
inter_ll L B C A O
inter_ll N B A C O
inter_ll M A C B O
A L
B M
C N
parallel O L A L
parallel O M B M
parallel O N C N O ** L / A ** L + O ** M / B ** M + O ** N / C ** N = 1.
Proof.
area_method.
Qed.

Theorem th6_7 :
A B C L M N O : Point,
inter_ll L B C A O
inter_ll N B A C O
inter_ll M A C B O
S A M L × (S B N M × S C L N) = S A N L × (S B L M × S C N M).
Proof.
area_method.
Qed.

Theorem th6_256_1 :
(A B C D P Q R S : Point) (r1 r2 : F),
on_parallel_d D A B C 1
on_line_d S D A r2
on_line_d P A B r1
on_line_d R C D r1
on_line_d Q B C r2
P S
parallel Q R P S.
Proof.
area_method.
Qed.

Theorem th6_257 :
(A B C D P Q R S : Point) (r1 r2 : F),
on_parallel_d D A B C 1
on_line_d S D A r2
on_line_d P A B r1
on_line_d R C D r1
on_line_d Q B C r2
S4 P Q R S = (2 × (r2 × r1) - r2 - r1 + 1) × S4 A B C D.
Proof.
area_method.
Qed.

Theorem gauss_line :
A0 A1 A2 A3 X Y M1 M2 M3 : Point,
inter_ll X A0 A3 A1 A2
inter_ll Y A2 A3 A1 A0
is_midpoint M1 A1 A3
is_midpoint M2 A0 A2
is_midpoint M3 X Y
S A0 A1 A2 0
Col M1 M2 M3.
Proof.
area_method.
Qed.