proposition: Lemma is_gravity_center_third_reci : forall A B C G A' A'', Midpoint A' B C -> Midpoint A'' A G -> Midpoint G A' A'' -> ~ Col A B C -> is_gravity_center G A B C.
proof: Proof. intros A B C G A' A'' HMid1 HMid2 HMid3 HNC. split; Col. Name B' the midpoint of A and C. Name C' the midpoint of A and B. exists A'; exists B'; split; [auto|]; split; [auto|]; split; [assert (A <> G) by (intro; treat_equalities; assert_cols; Col); assert_diffs; assert_cols; ColR|]. Name B'' the midpoint of B and G. assert (HB' := symmetric_point_construction B'' G). destruct HB' as [B''' HB']. assert (HPar1 : Par B A A' B'). { apply triangle_mid_par with C; assert_diffs; try split; unfold Midpoint in *; spliter; Between; Cong. } assert (HCong1 : Cong A C' A' B'). { assert (H := triangle_mid_par_cong A B C A' B' C'); destruct H as [Hc1 [Hc2 [Hc3 [H Hc4]]]]; assert_diffs; Cong. } assert (HPar2 : Par A B A'' B''). { apply triangle_mid_par with G; assert_diffs; try split; unfold Midpoint in *; spliter; Between; Cong. } assert (HCong2 : Cong A C' A'' B''). { assert (H := triangle_mid_par_cong A B G B'' A'' C'); destruct H as [Hc1 [Hc2 [Hc3 [H Hc4]]]]; assert_diffs; Cong; intro; treat_equalities; assert_cols; Col. assert_diffs; apply HNC; ColR. } assert (HPar3 : Par A'' B'' A' B'''). { apply plg_par_1; try (intro; treat_equalities; Col; assert_diffs; assert_cols; apply HNC; ColR). apply mid_plg_1 with G; try (intro; treat_equalities; assert_cols; Col); unfold Midpoint in *; spliter; split; Between; Cong. } assert (Cong3 : Cong A'' B'' A' B'''). { apply plg_cong_1. apply mid_plg_1 with G; try (intro; treat_equalities; assert_cols; Col); unfold Midpoint in *; spliter; split; Between; Cong. } assert (HCol : Col A' B' B'''). { assert (H := parallel_uniqueness A B A' B' A' B''' A'); destruct H as [HCol1 HCol2]; Col; Par. apply par_trans with A'' B''; Par. } assert (HElim := l7_20 A' B' B'''); elim HElim; clear HElim; try intro HElim; Col; try CongR. { assert (G <> B'') by (intro; treat_equalities; assert_cols; Col); ColR. } { assert (HFalse : OS A' B'' A'' B'''). { apply one_side_transitivity with G. { apply one_side_symmetry. assert (HH1 : A' <> B'') by (intro; treat_equalities; Col). assert (HH2 : Col A' B'' A') by Col. assert (HH3 : Col G A'' A') by (assert_cols; Col). assert (HH := l9_19 A' B'' G A'' A' HH2 HH3); rewrite HH. assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; Col. split; try (intro; treat_equalities; Col). unfold Midpoint in *; spliter; Between. } { assert (HH1 : A' <> B'') by (intro; treat_equalities; Col). assert (HH2 : Col A' B'' B'') by Col. assert (HH3 : Col G B''' B'') by (assert_cols; Col). assert (HH := l9_19 A' B'' G B''' B'' HH2 HH3); rewrite HH. assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; Col. split; try (intro; treat_equalities; Col). unfold Midpoint in *; spliter; Between. } } apply l9_9_bis in HFalse; exfalso; apply HFalse; clear HFalse. apply l9_8_2 with B'. { assert (A' <> B'') by (intro; treat_equalities; Col). assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; try (intro; apply HABG; ColR). exists A'; unfold Midpoint in *; spliter; split; Col; Between. } { apply one_side_transitivity with A. { apply one_side_symmetry; apply l9_17 with C; try (unfold Midpoint in *; spliter; assumption). apply one_side_transitivity with G. { apply one_side_symmetry. assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert (HH1 : A' <> B'') by (intro; treat_equalities; Col). assert (HH2 : Col A' B'' A') by Col. assert (HH3 : Col G A A') by ColR. assert (HH := l9_19 A' B'' G A A' HH2 HH3); rewrite HH. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; Col. split; try (intro; treat_equalities; Col). unfold Midpoint in *; spliter; eBetween. } { exists B; split. { assert (A' <> B'') by (intro; treat_equalities; Col). assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; try (intro; apply HABG; ColR). exists B''; unfold Midpoint in *; spliter; split; Col; Between. } { assert (A' <> B'') by (intro; treat_equalities; Col). assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). split; try (intro; apply HABG; ColR). split; try (intro; apply HABG; ColR). exists A'; unfold Midpoint in *; spliter; split; Col; Between. } } } { assert_diffs; assert_cols; show_distinct G A'; treat_equalities; Col. show_distinct G A''; treat_equalities; Col. show_distinct G B''; treat_equalities; Col. assert (HH1 : A' <> B'') by (intro; treat_equalities; Col). assert (HH2 : Col A' B'' A') by Col. assert (HH3 : Col A A'' A') by ColR. assert (HH := l9_19 A' B'' A A'' A' HH2 HH3); rewrite HH. assert_diffs; assert_cols; assert (HABG : ~ Col A B G) by (intro; apply HNC; ColR). show_distinct A A'; Col. split; try (intro; apply HABG; ColR). split; Col. split; try (intro; treat_equalities; Col). unfold Midpoint in *; spliter; eBetween. } } } Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon