proposition: Lemma is_gravity_center_diff_2 : forall A B C G, is_gravity_center G A B C -> G<>B.
proof: Proof. intros. intro. unfold is_gravity_center in *. spliter. decompose [ex and] H1. assert_cols. apply H. treat_equalities. assert_diffs. ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon