proposition: Lemma sesamath_4ieme_G2_ex41 : forall (T L H O E S A: Tpoint) (a b : Tpoint ->Tpoint ->Tpoint -> Prop), ~ Col T L H -> Midpoint E T L -> Midpoint O T H -> A <> T -> A <> O -> A <> E -> A <> S -> Bet T A S -> Bet O A E -> Bet H S L -> S <> H -> S <> L -> CongA S A E T S H /\ Midpoint A T S.
proof: Proof. intros. assert_diffs. assert_cols. assert(OS H L T T) by (apply(one_side_reflexivity H L T);finish). assert(OS H S T T) by(apply(col_one_side H L S T T);finish). assert(~ Col H S T) by(apply(one_side_not_col123 H S T T);finish). assert( OS T S H H) by(apply(one_side_reflexivity T S H);finish). assert(OS T A H H) by(apply(col_one_side T S A H H);finish). assert(Bet T O H) by(apply(midpoint_bet T O H);finish). assert(Out T O H) by(apply(bet_out T O H);finish). assert(Out T H O) by(apply(l6_6 T O H);finish). assert(OS T A H O) by(apply(out_out_one_side T A H H O);finish). assert(OS T A O H) by(apply(one_side_symmetry T A H O);finish). assert(Par H L O E) by(apply(triangle_mid_par H L T E O);finish). assert(Par H L O A) by(apply(par_col_par H L O E A);finish). assert(Par H S O A) by(apply(par_col_par_2 H L O A S);finish). assert(Out T A S) by(apply(bet_out T A S);finish). assert(CongA O A T H S T) by(apply(l12_22_a A O S H T);finish). assert(CongA O A T E A S) by(apply(l11_14 O A T E S);finish). assert(CongA H S T E A S) by(apply(conga_trans H S T O A T E A S);finish). assert(Midpoint A S T) by(apply(triangle_par_mid S H T O A);finish). split;finish. Qed.
imports: GeoCoq.Highschool.triangles GeoCoq.Highschool.circumcenter GeoCoq.Highschool.gravityCenter