proposition: Lemma is_gravity_center_third : forall A B C G G' A', is_gravity_center G A B C -> Midpoint G' A G -> Midpoint A' B C -> Midpoint G A' G'.
proof: Proof. intros. Name C' the midpoint of A and B. assert (Col G C' C) by (apply is_gravity_center_col with A B; Col). unfold is_gravity_center in *. spliter. destruct H4 as [A'' [B' HIJ]]. spliter. treat_equalities. assert_diffs. Name G'' the midpoint of C and G. assert (HPar : Parallelogram C' A' G'' G'). apply (varignon' A B C G C' A' G'' G'); finish. apply parallelogram_to_plg in HPar. destruct HPar as [HDiff [I [HCol1 HCol2]]]. assert (G = I); [|subst; Cong]. show_distinct G A; [apply H; ColR|]. assert (~ Col A G C) by (intro; apply H; ColR). assert (C' <> G'' /\ A' <> G') by (elim HDiff; clear HDiff; intro; split; trivial; intro; apply H; ColR). spliter. assert_diffs. apply l6_21 with A G C G; trivial; ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon