# Library AreaMethod.examples_centroid

Require Export area_method.

Lemma centroid_check : A B C G A',
is_centroid G A B C
is_midpoint A' B C
Col A G A'.
Proof.
area_method.
Qed.

Lemma euler_line : 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.
area_method.
Qed.

Lemma centroid_midpoint_centroid : 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+20
Col G G' X.
Proof.
area_method.
Qed.

Lemma centroid_midpoint_centroid_2 : 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+20
Py G G' G = 0.
Proof.
geoInit.
eliminate G'.
eliminate A'.
eliminate B'.
eliminate C'.
eliminate G.
unfold_Py.
uniformize_dir_seg.
field_and_conclude.
Qed.

Lemma l6_44 : 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
GQ GP 1+2 0
2×2×S4 P Q C B = (2+2+1)* S A Q P.
Proof.
area_method.
Qed.

Lemma l6_47 : 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 AM AN
parallel N C A N BM
1+2 0 2+1 0
M**B/A**M + N**C/A**N = 1.
Proof.
geoInit.
am_before_field.
field;solve_conds.
intro.
replace (- (f × (/ (2 + 1) × S C A B))) with (- (f × S C A B) / (2+1)) in H7 by (field;solve_conds).
rewrite H13 in H7.
replace (0 / (2 + 1)) with (0) in H7 by (field;solve_conds).
intuition.
intuition.
intuition.
Qed.