proposition: Lemma intersection_two_medians_exist_unique : forall A B C I J, ~Col A B C -> Midpoint I B C -> Midpoint J A C -> exists! G, Col G A I /\ Col G B J.
proof: Proof. Proof with finish. intros. elim (intersection_two_medians_exist A B C I J H H0 H1); intros G HG; spliter. exists G. unfold unique. assert_all. repeat split... intros G' HG'; spliter. apply l6_21 with A I B J... intro; search_contradiction. show_distinct' B J... Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon