proposition: Lemma intersection_two_medians_exist : 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. assert_bets. elim (inner_pasch A B C J I)... intro G;intros. exists G. spliter;assert_cols;split... Qed.
imports: GeoCoq.Tarski_dev.Annexes.midpoint_theorems GeoCoq.Highschool.varignon