proposition: Lemma inter_circle : forall P Q A T M, Cong P A Q A -> Le P M P A -> Le Q M Q A -> Projp A T P Q -> Le T M T A.
proof: Proof. intros. assert(HH:= circle_projp_between P Q A T H H2). induction(eq_dec_points T M). { subst M. apply le_trivial. } { induction(eq_dec_points P T). { treat_equalities; auto. } assert(HA:= angle_partition P T M H4 H3). induction(eq_dec_points Q T). { treat_equalities; auto. } { induction HA. { assert(HB:= acute_bet__obtuse P T M Q HH H5 H6). apply(inter_circle_obtuse Q P); Cong. unfold Projp in *. spliter. split; auto. induction H7. { left. spliter. split; Col; Perp. } { right. spliter. split; Col. } } { apply(inter_circle_obtuse P Q); Cong. induction H6. { right; auto. } { left; auto. } } } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order