proposition: Lemma construct_triangle : forall A B C, ~ Col A B C -> exists D, exists E, exists F, Col B D F /\ Col A E F /\ Col C D E /\ Par A B C D /\ Par A C B D /\ Par B C A E /\ Par A B C E /\ Par A C B F /\ Par B C A F /\ D <> E /\ D <> F /\ E <> F.
proof: Proof. intros A B C HNC. assert_diffs; rename H2 into HAB; rename H1 into HBC; rename H4 into HAC. elim (parallel_existence1 A B C HAB);intros X1 HX1. elim (parallel_existence1 A C B HAC);intros X2 HX2. elim (parallel_existence1 B C A HBC);intros X3 HX3. assert (T : exists D, Col D B X2 /\ Col D C X1) by (apply construct_intersection with A X3; finish); DecompExAnd T D. assert (T : exists E, Col E A X3 /\ Col E C X1) by (apply construct_intersection with B X2; finish); DecompExAnd T E. assert (T : exists F, Col F A X3 /\ Col F B X2) by (apply construct_intersection with C X1; finish); DecompExAnd T F. assert (A <> E) by (apply not_col_par_col_diff with B C X1; finish). assert (A <> F) by (apply not_col_par_col_diff with C B X2; finish). assert (B <> D) by (apply not_col_par_col_diff with A C X1; finish). assert (B <> F) by (apply not_col_par_col_diff with C A X3; finish). assert (C <> D) by (apply not_col_par_col_diff with A B X2; finish). assert (C <> E) by (apply not_col_par_col_diff with B A X3; finish). assert (Par A B C D) by (apply par_col_par with X1; finish). assert (Par A C B D) by (apply par_col_par with X2; finish). assert (Par B C A E) by (apply par_col_par with X3; finish). assert (Par A B C E) by (apply par_col_par with X1; finish). assert (Par A C B F) by (apply par_col_par with X2; finish). assert (Par B C A F) by (apply par_col_par with X3; finish). assert (~ (D = E /\ D = F)). intro; spliter; treat_equalities. assert_paras_perm. assert_nparas_perm. permutation_intro_in_hyps. contradiction. exists D; exists E; exists F. assert_diffs. repeat split; try ColR; finish. intro; subst. assert (E <> F) by (intro; subst; intuition). apply HNC; apply col_permutation_1; apply not_strict_par1 with E A; sfinish. intro; subst. assert (E <> F) by (intro; subst; intuition). apply HNC; apply col_permutation_2; apply not_strict_par1 with E C; sfinish. intro; subst. assert (D <> F) by (intro; subst; intuition). apply HNC; apply not_strict_par1 with D B; sfinish. Qed.
imports: GeoCoq.Highschool.circumcenter