# Library AreaMethod.examples_5

Require Import area_method.

Lemma l6_17 : A B R P Q S C F,
on_line P B R
on_line Q A R
inter_ll S A P B Q
inter_ll C R S A B
inter_ll F P Q A B
parallel A C B C
parallel A F B F
BC BF
A**C / B**C = - A**F / B**F.
Proof.
area_method.
Qed.

Lemma l6_52 : A B C D E F,
is_midpoint E A C
is_midpoint F A B
is_midpoint D B C
2*(Py A D A)+2*(Py F C F) +2×Py B E B =
(2+1)/2 × (Py A C A + Py A B A + Py B C B).
Proof.
area_method.
Qed.

Lemma l6_55 : A B C E G,
is_midpoint E A C
on_line_d G B E (2/(2+1))
1+2 0
(2+1) × (Py A G A + Py G C G + Py B G B) =
Py A C A + Py A B A + Py B C B.
Proof.
area_method.
Qed.

Lemma l6_56 : A B C E G M,
is_midpoint E A C
on_line_d G B E (2/(2+1))
1+2 0
(2+1) × Py M G M + Py A G A + Py G C G + Py B G B =
Py A M A + Py B M B + Py C M C.
Proof.
area_method.
Qed.

Lemma l6_67 : A B C F E,
on_foot F C A B
on_foot E B A C
Py B A F = Py C A E.
Proof.
area_method.
Qed.

Lemma l6_69 : A B C D E F,
on_foot F C A B
on_foot E B A C
on_foot D A B C
eq_angle E D C B D F.
Proof.
area_method.
Qed.

Lemma l6_197 : A B C E F G,
on_foot E A B C
on_foot F B A C
on_foot G C A B
2 × Py A B C × Py B A C × Py A C B × S A B C =
Py A B A × Py B C B × Py A C A × S E F G.
Proof.
area_method.
Qed.

Lemma l6_218 : 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
2× S4 E F G H = S4 A B C D.
Proof.
area_method.
Qed.

Lemma l6_224 : A B C D N M P r,
is_midpoint N A C
is_midpoint M B D
on_line_d P N M r
S P A B + S P C D = S P D A + S P B C.
Proof.
area_method.
Qed.

Lemma l6_223 : A B C D X Y W,
is_midpoint X C A
is_midpoint Y B D
inter_ll W B C D A
S4 B C D A = (2+2)* S X Y W.
Proof.
am_before_field.
field_simplify_eq.
2:solve_conds.
ring_simplify_eq.
only_use_area_coordinates.
field_and_conclude.
Qed.