proposition: Lemma sesamath_4ieme_G2_ex39: forall S C T H A, ~Col A C T -> is_circumcenter S C T A-> Midpoint S C T -> Col C H A -> Perp S H A C -> Midpoint H A C.
proof: Proof. intros. assert_diffs. assert_cols. assert (Cong C S T S /\ Cong T S A S /\ Cong A S C S) by ( apply(circumcenter_cong S C T A);finish). spliter. assert(Per C A T) by (perm_apply(midpoint_thales S C T A);finish). assert(Perp T A A C) by finish. assert(Par S H T A) by (perm_apply(l12_9 S H T A A C);finish). assert(Midpoint H A C) by (perm_apply(triangle_par_mid A T C S H);finish). assumption. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter