proposition: Lemma inter_circle_per : 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 -> 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(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. apply sum_comm in Pyth; auto. apply sum_diff in Pyth. 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(PythM : Sum O E E' PT2 TM2 PM2). { apply(pythagoras O E E' P M T PT TM PM PT2 TM2 PM2 HX); auto. apply length_sym;auto. } assert(SS'=PM2). { apply (sum_uniqueness O E E' PT2 TM2); auto. } subst SS'. induction(eq_dec_points T M). { subst T. 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. apply(sum_pos_null) in H33. spliter. subst PT2. apply prod_null in H17. induction H17. { subst PT. apply length_cong in H14. treat_equalities. tauto. } { subst PT. apply length_cong in H14. treat_equalities. tauto. } apply (square_not_neg O E E' PT); auto. apply (square_not_neg O E E' TM); auto. } { 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. unfold Ar2. repeat split; auto. apply (length_Ps O E E' P M); auto. intro. treat_equalities. set(O:=PA) in *. subst PM. assert(PM2=O). { apply(prod_O_l_eq O E E' O);auto. } subst PM2. apply length_id_1 in H29. contradiction. apply length_pos_or_null in H16. induction H16. { assumption. } { treat_equalities. assert(HH:= length_id_2 O E E' Q HX). assert(HP:=length_uniqueness O E E' Q Q O PM HH H29). treat_equalities. apply(prod_O_l_eq)in H32. subst PM2. apply sum_pos_null in H33. spliter; tauto. apply(square_not_neg O E E' PT PT2 H17). apply(square_not_neg O E E' TM TM2 H31). } } apply sum_comm in H33; auto. apply sum_comm in H20; auto. assert(HH:=sum_preserves_lep_rev O E E' TM2 TA2 PT2 PM2 AP2 H33 H20 H30). induction(eq_dec_points TA TM). { treat_equalities. assert(Cong T M T A). { apply(length_eq_cong_1 O E E' _ _ _ _ TA); auto. } apply cong__le; auto. } assert(LtP O E E' TM2 TA2). { apply(lep_neq__ltp O E E'). split; auto. intro. apply H34. subst TM2. apply(root_uniqueness O E E' TA TM TA2); auto. apply(length_not_neg O E E' T A); auto. apply(length_not_neg O E E' T M); auto. } assert(LtP O E E' TM TA). { apply (square_increase_rev O E E' TM TA TM2 TA2); auto. apply length_Ps in H28; auto. intro. subst TM. apply length_id_1 in H28. tauto. apply length_Ps in H15; auto. intro. subst TA. apply length_id_1 in H15. subst T. apply perp_distinct in H6. tauto. } apply lt__le. apply (ltp_to_lt O E E' T M TM T A 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