proposition: Lemma is_gravity_center_perm_1 : forall A B C G, is_gravity_center G A B C -> is_gravity_center G A C B.
proof: Proof. intros. apply is_gravity_center_perm in H;intuition. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon