proposition: Lemma onc2_mid__incs : forall O P U V M, U <> V -> OnCircle U O P -> OnCircle V O P -> Midpoint M U V -> InCircleS M O P.
proof: Proof. intros O P U V M HUV HUOn HVOn HM. assert_diffs. apply bet_inc2__incs with U V; Between; Circle. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel