proposition: Lemma onc2_mid_cong_col : forall O P U V M X, U <> V ->OnCircle U O P -> OnCircle V O P -> Midpoint M U V -> Cong U X V X -> Col O X M.
proof: Proof. intros. assert(HH:=mid_onc2__per O P U V M H0 H1 H2). assert(Per X M U). unfold Per. exists V. unfold OnCircle in *. split; Cong. apply(per2__col _ _ U); auto. assert_diffs. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel