proposition: Lemma nine_point_circle : forall A B C A1 B1 C1 A2 B2 C2 A3 B3 C3 H O, ~ Col A B C -> Col A B C2 -> Col B C A2 -> Col A C B2 -> Perp A B C C2 -> Perp B C A A2 -> Perp A C B B2 -> Perp A B C2 H -> Perp B C A2 H -> Perp A C B2 H -> Midpoint A3 A H -> Midpoint B3 B H -> Midpoint C3 C H -> Midpoint C1 A B -> Midpoint A1 B C -> Midpoint B1 C A -> Cong O A1 O B1 -> Cong O A1 O C1 -> Cong O A2 O A1 /\ Cong O B2 O A1 /\ Cong O C2 O A1 /\ Cong O A3 O A1 /\ Cong O B3 O A1 /\ Cong O C3 O A1.
proof: Proof. intros A B C A1 B1 C1 A2 B2 C2 A3 B3 C3 H O0; convert_to_algebra. decompose_coordinates; intros; spliter. clear H24; clear H25; clear H26; clear H27; clear H28; clear H29; clear H30; clear H31; clear H32; clear H33; clear H34; clear H35; put_negs_in_goal. scnf; [ .. |spliter; rtauto]; express_disj_as_a_single_poly; (assert (Nsat2 : ~ ((2) =F= 0)) by prove_discr_for_powers_of_2; assert (Nsatm2 : ~ (-(2) =F= 0)) by prove_discr_for_powers_of_2; nsatz). Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems