proposition: Lemma inter_circle_obtuse : 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 -> Obtuse P T M \/ Per P T M -> Le T M T A.
proof: Proof. intros. assert(HH:=lower_dim). set(O:=PA) in *. set(E:=PB) in *. set(E':=PC) in *. assert(HD:~Col O E E'). intro. apply HH. unfold Col in H4. tauto. clear HH. induction(eq_dec_points P T). { subst T. auto. } { unfold Projp in H2. spliter. induction H5. spliter. assert(HX:O<>E). { assert_diffs; auto. } assert(Per P T A). { apply (perp_col _ _ _ _ T) in H6; auto. apply perp_left_comm in H6. apply perp_perp_in in H6. apply perp_in_comm in H6. apply perp_in_per in H6. assumption. } assert(Py:= pyth_context O E E' P T A HD). ex_and Py PT . ex_and H8 TA . ex_and H9 AP. ex_and H8 PT2. ex_and H9 TA2. ex_and H8 AP2. ex_and H9 SS. assert(Py:= pyth_context O E E' P T M HD). ex_and Py PT' . ex_and H21 TM . ex_and H22 PM. ex_and H21 PT2'. ex_and H22 TM2. ex_and H21 PM2. ex_and H22 SS'. assert(PT=PT'). { apply (length_uniqueness O E E' P T); auto. } subst PT'. assert(PT2=PT2'). { apply (prod_uniqueness O E E' PT PT); auto. } subst PT2'. clean_duplicated_hyps. assert(Pyth : Sum O E E' PT2 TA2 AP2). { apply(pythagoras O E E' P A T PT TA AP PT2 TA2 AP2 HX); auto. apply length_sym;auto. } assert(HE: SS = AP2). { apply(sum_uniqueness O E E' PT2 TA2); auto. } subst SS. assert(Pyth1 : LeP O E E' SS' PM2). { apply(pythagoras_obtuse_or_per O E E' P M T PT TM PM PT2 TM2 PM2 SS'); auto. apply length_sym; auto. } induction(eq_dec_points T M). { subst M. apply le_trivial. } { induction(eq_dec_points P M). { subst M. assert(HH:= length_id_2 O E E' P HX). assert(PM = O). { apply (length_uniqueness O E E' P P); auto. } subst PM. assert(PM2=O). { apply(prod_O_l_eq O E E' O);auto. } subst PM2. assert(Ps O E SS'). { apply(sum_pos_pos O E E' PT2 TM2 SS'); auto. apply (square_pos O E E' PT); auto. intro. subst PT. apply length_cong in H14. apply cong_identity in H14. contradiction. apply (square_pos O E E' TM); auto. intro. subst TM. apply length_cong in H28. apply cong_identity in H28. contradiction. } unfold LeP in Pyth1. induction Pyth1. apply (ltP_neg) in H27. apply pos_not_neg in H24. contradiction. subst SS'. unfold Ps in H24. unfold Out in H24;tauto. } assert(LeP O E E' PM AP). { apply(length_leP_le_2 O E E' P M P A PM AP); auto. } assert(LeP O E E' PM2 AP2). { apply(square_increase O E E' PM AP); auto. repeat split; auto. apply length_pos_or_null in H29. induction H29. { auto. } { treat_equalities; tauto. } apply length_pos_or_null in H16. induction H16. { auto. } { treat_equalities; tauto. } } assert(LeP O E E' SS' AP2). { apply (leP_trans O E E' SS' PM2 AP2); auto. } assert(LeP O E E' TM2 TA2). { apply(sum_preserves_lep_rev O E E' TM2 TA2 PT2 SS' AP2); auto. apply sum_comm; auto. apply sum_comm; auto. } assert(Ps O E TM). { apply length_pos_or_null in H28. induction H28. { auto. } { treat_equalities; tauto. } } assert(Ps O E TA). { apply length_pos_or_null in H15. induction H15. { auto. } { subst T. apply perp_distinct in H6; tauto. } } assert(LeP O E E' TM TA). { induction(eq_dec_points TM TA). { subst TM. apply leP_refl. } { apply ltp_to_lep. apply (square_increase_rev O E E' TM TA TM2 TA2); auto. apply(lep_neq__ltp O E E'). split; auto. intro. apply H38. subst TM2. apply (root_uniqueness O E E' TM TA TA2); auto. intro. apply pos_not_neg in H36. contradiction. intro. apply pos_not_neg in H37. contradiction. } } apply(length_leP_le_1 O E E' T M T A TM TA); auto. } { spliter. assert(HH:=(inter_tangent_circle P Q A M H2 H)). assert(M = A). { apply HH; Col. } subst M. apply le_reflexivity. } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order