proposition: Lemma ColCongMid: forall A B C, A <> C -> Col A B C -> Cong A B B C -> Midpoint B A C.
proof: Proof. intros. assert(Col A B C). Col. assert(Cong B A B C). Cong. assert(A = C \/ Midpoint B A C). apply l7_20; tauto. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect