proposition: Lemma is_gravity_center_perm : forall A B C G, is_gravity_center G A B C -> is_gravity_center G A B C /\ is_gravity_center G A C B /\ is_gravity_center G B A C /\ is_gravity_center G B C A /\ is_gravity_center G C A B /\ is_gravity_center G C B A.
proof: Proof. intros. Name I the midpoint of A and B. assert (Col G I C) by (apply is_gravity_center_col with A B;finish). unfold is_gravity_center in *. spliter. destruct H2 as [J [K [Ha [Hb [Hc Hd]]]]]. repeat split;Col. exists J; exists K;repeat (split;finish). exists J; exists I;repeat (split;finish). exists K; exists J;repeat (split;finish). exists K; exists I;repeat (split;finish). exists I; exists J;repeat (split;finish). exists I; exists K;repeat (split;finish). Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon