proposition: Lemma l15_7 : forall O E E' A B C H AB AC AH AC2, O<>E -> Per A C B -> Perp_at H C H A B -> Length O E E' A B AB -> Length O E E' A C AC -> Length O E E' A H AH -> (Prod O E E' AC AC AC2 <-> Prod O E E' AB AH AC2).
proof: Proof. intros. induction(eq_dec_points AB O). subst AB. assert(A = B). apply (length_id_1 O E E'); assumption. subst B. apply perp_in_distinct in H2. tauto. assert(~Col O E E' /\ Col O E AB). unfold Length in H3. spliter. unfold LeP in H8. induction H8. unfold LtP in H8. ex_and H8 X. apply diff_sum in H8. apply sum_ar2 in H8. unfold Ar2 in H8. tauto. subst AB. tauto. spliter. induction(eq_dec_points H A). subst H. assert(AH=O). apply (length_uniqueness O E E' A A); auto. apply length_id_2. assumption. subst AH. apply perp_in_per in H2. assert(A = C). apply (l8_7 B); Perp. subst C. assert(AC = O). apply (length_uniqueness O E E' A A); auto. subst AC. split;intros; assert(AC2=O). apply (prod_uniqueness O E E' O O); auto. apply prod_0_r; Col. subst AC2. apply prod_0_r; Col. apply (prod_uniqueness O E E' AB O); auto. apply prod_0_r; Col. subst AC2. apply prod_0_r; Col. assert(C <> A). intro. subst C. apply perp_in_right_comm in H2. apply perp_in_id in H2. contradiction. assert(HH:= segment_construction_2 H A A C H9). ex_and HH C'. assert(Out A H C'). unfold Out. repeat split; auto. intro. subst C'. apply cong_symmetry in H12. apply cong_identity in H12. subst C. tauto. assert(HH:= segment_construction_2 C A A H H10). ex_and HH H'. assert(Out A C H'). repeat split;auto. intro. subst H'. apply cong_symmetry in H15. apply cong_identity in H15. subst H. tauto. assert(H <> C). intro. subst H. apply perp_in_distinct in H2. tauto. assert(Cong H C H' C' /\ (H <> C -> CongA A H C A H' C' /\ CongA A C H A C' H')). apply(l11_49 H A C H' A C'). apply conga_left_comm. apply out2__conga. apply l6_6. assumption. apply l6_6. assumption. Cong. Cong. spliter. assert(HH:= H19 H17). clear H19. spliter. assert(Per A H C). apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_comm. apply (perp_col _ B). auto. apply perp_in_perp_bis in H2. induction H2. apply perp_distinct in H2. tauto. apply perp_sym. apply perp_left_comm. assumption. apply perp_in_col in H2. tauto. assert(HH:= l11_17 A H C A H' C' H21 H19). assert(Par C B H' C'). apply(l12_9_2D C B H' C' A C). apply per_perp_in in H1. apply perp_in_comm in H1. apply perp_in_perp_bis in H1. induction H1. Perp. apply perp_distinct in H1. tauto. auto. intro. subst C. apply perp_in_id in H2. contradiction. apply per_perp_in in HH. apply perp_in_comm in HH. apply perp_in_perp_bis in HH. apply perp_sym. apply perp_right_comm. apply(perp_col A H' C' H' C). auto. induction HH. Perp. apply perp_distinct in H22. tauto. apply out_col in H16. Col. intro. subst H'. apply conga_distinct in H19. tauto. intro. subst H'. apply conga_distinct in H19. tauto. assert(HL1:=length_existence O E E' A H' H7). ex_and HL1 AH'. assert(HL1:=length_existence O E E' A C' H7). ex_and HL1 AC'. assert(exists P : Tpoint, Prod O E E' AC' AC P). apply(prod_exists O E E' H7 AC' AC). unfold Length in H24. tauto. unfold Length in H4. tauto. ex_and H25 P. assert(Perp C H A B). apply perp_in_perp_bis in H2. induction H2. apply perp_distinct in H2. tauto. assumption. assert(Prodg O E E' AH' AB P). apply(thales O E E' A C' B H' C AC' AB AH' AC P); Col. apply perp_in_col in H2. spliter. apply out_col in H13. ColR. apply out_col in H16. Col. intro. assert(Perp H A C H). apply perp_comm. apply(perp_col A B H C H). intro. subst H. apply conga_distinct in H19. tauto. Perp. apply perp_in_col in H2. tauto. apply perp_not_col in H28. apply H28. assert(A <> C'). intro. subst C'. unfold CongA in H20. tauto. assert(Col A H H'). ColR. assert(A <> H'). intro. subst H'. unfold CongA in H19. tauto. ColR. left. Par. left. assumption. assert(Prod O E E' AH' AB P). induction H27. assumption. spliter. apply False_ind. apply H27. repeat split; Col. unfold Length in H23. tauto. assert(Length O E E' A H' AH). apply(length_eq_cong_2 O E E' A H A H' AH H5). Cong. assert(AH = AH'). apply (length_uniqueness O E E' A H'); auto. subst AH'. assert(Length O E E' A C' AC). apply(length_eq_cong_2 O E E' A C A C' AC H4). Cong. assert(AC = AC'). apply (length_uniqueness O E E' A C'); auto. subst AC'. split. intro. assert(P = AC2). apply (prod_uniqueness O E E' AC AC); auto. subst P. apply prod_comm. assumption. intro. assert(P = AC2). apply (prod_uniqueness O E E' AB AH); auto. apply prod_sym. assumption. subst P. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order