proposition: Lemma circle_projp_between : forall P Q A T, Cong P A Q A -> Projp A T P Q -> Bet P T Q.
proof: Proof. intros. induction(eq_dec_points P T). { subst T; Between. } { unfold Projp in H0. spliter. induction H2. { spliter. assert(Per A T P). { apply (perp_col _ _ _ _ T) in H3; auto. apply perp_left_comm in H3. apply perp_perp_in in H3. apply perp_in_comm in H3. apply perp_in_per in H3. apply l8_2. assumption. } assert(HM:=midpoint_existence P Q). ex_and HM T'. assert(Per A T' P). { unfold Per. exists Q. split; Cong. } assert(T' = T \/ ~ Col T P Q). { apply(col_per2_cases A T' P Q T); Col. intro. treat_equalities. apply perp_distinct in H3; tauto. } induction H7. subst T'. Between. assert(Col T A T'). { apply(col_perp2_ncol__col A T A T' P Q); Col. Perp. apply per_perp_in in H6. apply perp_in_comm in H6. apply perp_in_perp in H6. apply perp_sym in H6. apply perp_sym. apply (perp_col _ T'); Perp; Col. intro. treat_equalities. unfold Midpoint in H5; spliter. apply H7; ColR. intro. subst T'. apply is_midpoint_id in H5. contradiction. intro. apply H7. ColR. } assert(T=T'). { apply(per2_col_eq A T T' P); Perp. intro. treat_equalities. apply perp_distinct in H3; tauto. intro. treat_equalities. unfold Midpoint in H5; spliter. apply H7; ColR. } subst T'. Between. } spliter. subst T. assert(P = Q \/ Midpoint A P Q). { apply(l7_20 A P Q); Col. Cong. } induction H3. { contradiction. } Between. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order