proposition: Lemma is_gravity_center_cases : forall A B C G, 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 -> is_gravity_center G A B C.
proof: Proof. intros. decompose [or] H;clear H. apply is_gravity_center_perm in H0;intuition. apply is_gravity_center_perm in H1;intuition. apply is_gravity_center_perm in H0;intuition. apply is_gravity_center_perm in H1;intuition. apply is_gravity_center_perm in H0;intuition. apply is_gravity_center_perm in H0;intuition. Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon