proposition: Lemma diam_cong_incs__outcs : forall O P A B U V, Diam A B O P -> Cong A B U V -> InCircleS U O P -> OutCircleS V O P.
proof: Proof. intros. induction(eq_dec_points O P). treat_equalities. unfold InCircleS in H1. unfold Lt in H1. spliter. apply le_zero in H1. treat_equalities. apply False_ind. apply H2; Cong. assert(HH:= circle_cases O P V). induction HH. assert(Lt U V A B) by apply(incs_onc_diam__lt O P A B U V H H1 H3). unfold Lt in H4. spliter. apply False_ind. apply H5; Cong. induction H3. assert(HH:=incs2_lt_diam O P A B U V H H1 H3). unfold Lt in HH. spliter. apply False_ind. apply H5; Cong. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel