proposition: Lemma triangular_equality_bis : forall O E E' A B C AB BC AC, A <> B \/ A <> C \/ B <> C -> O<>E -> Bet A B C -> Length O E E' A B AB -> Length O E E' B C BC -> Length O E E' A C AC -> Sum O E E' AB BC AC.
proof: Proof. intros O E E' A B C AB BC AC. intro HH0. intros. unfold Length in *. spliter. unfold LeP in *. induction H11; induction H8; induction H5. unfold LtP in *. ex_and H11 X. ex_and H8 Y. ex_and H5 Z. apply diff_sum in H11. apply diff_sum in H8. apply diff_sum in H5. assert(AB = X). apply (sum_uniqueness O E E' O X). assumption. unfold Sum in H11. spliter. unfold Ar2 in H11. apply(sum_O_B); tauto. subst X. assert(BC = Y). apply (sum_uniqueness O E E' O Y). assumption. unfold Sum in H8. spliter. unfold Ar2 in H8. apply(sum_O_B); tauto. subst Y. assert(AC = Z). apply (sum_uniqueness O E E' O Z). assumption. unfold Sum in H5. spliter. unfold Ar2 in H5. apply(sum_O_B); tauto. subst Z. assert(forall A B : Tpoint,Col O E A -> Col O E B -> exists C : Tpoint, Sum O E E' A B C). apply(sum_exists O E E' ). unfold Sum in H11. spliter. unfold Ar2 in H11. tauto. assert(HS:= H16 AB BC H10 H7). ex_and HS AC'. assert(Bet O AB AC'). apply(l14_36_a O E E' AB BC AC' H17). eapply (l6_7 _ _ E). assumption. apply l6_6. assumption. assert(HH:= l15_3 O E E' AB BC AC' H17). assert(Cong O AC' A C). apply(l2_11 O AB AC' A B C); Cong. apply cong_transitivity with O BC; Cong. assert(HP:= sum_pos_pos O E E' AB BC AC' H13 H14 H17). assert(AC = AC'). apply(l6_11_uniqueness O A C E AC AC'). unfold Ps in H15. assumption. Cong. unfold Ps in HP. assumption. Cong. subst AC'. assumption. subst AC. apply cong_symmetry in H6. apply cong_identity in H6. subst C. apply between_identity in H0. subst B. apply cong_identity in H12. subst AB. apply cong_identity in H9. subst BC. unfold LtP in H8. ex_and H8 X. apply diff_sum in H0. assert(X=O). apply(sum_uniqueness O E E' O X). apply sum_O_B. unfold Sum in H0. spliter. unfold Ar2 in H0. tauto. unfold Ps in H5. apply out_col in H5. Col. assumption. subst X. unfold Ps in H5. unfold Out in H5. tauto. subst BC. apply cong_symmetry in H9. apply cong_identity in H9. subst C. assert(Cong O AB O AC). apply cong_transitivity with A B; Cong. unfold LtP in H11. ex_and H11 X. apply diff_sum in H9. assert(X = AB). apply (sum_uniqueness O E E' O X). apply sum_O_B. unfold Sum in H9. spliter. unfold Ar2 in H9. tauto. unfold Ps in H11. apply out_col in H11. Col. assumption. subst X. unfold LtP in H5. ex_and H5 Y. apply diff_sum in H5. assert(Y = AC). apply (sum_uniqueness O E E' O Y). apply sum_O_B. unfold Sum in H9. spliter. unfold Ar2 in H9. tauto. unfold Ps in H13. apply out_col in H13. Col. assumption. subst Y. assert(AB = AC). apply(l6_11_uniqueness O A B E AB AC). unfold Ps in H11. assumption. Cong. unfold Ps in H13. assumption. Cong. subst AB. apply sum_A_O. unfold Sum in H9. unfold Ar2 in H9. tauto. unfold Ps in H11. apply out_col in H11. Col. subst AC. subst BC. apply cong_symmetry in H6. apply cong_identity in H6. subst C. apply cong_symmetry in H9. apply cong_identity in H9. subst B. apply cong_identity in H12. subst AB. apply sum_O_O. unfold LtP in H11. ex_and H11 X. apply diff_sum in H5. unfold Sum in H5. unfold Ar2 in H5. tauto. subst AB. apply cong_symmetry in H12. apply cong_identity in H12. subst B. assert(BC = AC). apply(l6_11_uniqueness O A C E BC AC). unfold LtP in H8. ex_and H8 X. apply diff_sum in H8. assert(X = BC). apply (sum_uniqueness O E E' O X). apply sum_O_B. unfold Sum in H8. unfold Ar2 in H8. tauto; unfold Out in H13. unfold Ps in H11. apply out_col in H11. Col. assumption. subst X. unfold Ps in H11. assumption. Cong. unfold LtP in H5. ex_and H5 X. apply diff_sum in H5. assert(X = AC). apply (sum_uniqueness O E E' O X). apply sum_O_B. unfold Sum in H5. unfold Ar2 in H5. tauto; unfold Out in H13. unfold Ps in H11. apply out_col in H11. Col. assumption. subst X. unfold Ps in H11. assumption. Cong. subst AC. apply sum_O_B. unfold LtP in H5. ex_and H5 X. apply diff_sum in H5. unfold Sum in H5. unfold Ar2 in H5. tauto. Col. subst AC. subst AB. apply cong_symmetry in H12. apply cong_identity in H12. subst B. apply cong_symmetry in H6. apply cong_identity in H6. subst C. apply cong_identity in H9. subst BC. apply sum_O_O. unfold LtP in H8. ex_and H8 X. apply diff_sum in H5. unfold Sum in H5. unfold Ar2 in H5. tauto. subst AB. subst BC. apply cong_symmetry in H9. apply cong_identity in H9. subst C. apply cong_symmetry in H12. apply cong_identity in H12. subst B. apply cong_identity in H6. subst AC. apply sum_O_O. unfold LtP in H5. ex_and H5 X. apply diff_sum in H5. unfold Sum in H5. unfold Ar2 in H5. tauto. subst AB. subst AC. subst BC. apply cong_symmetry in H12. apply cong_identity in H12. subst B. apply cong_symmetry in H9. apply cong_identity in H9. subst C. apply cong_identity in H6. induction HH0; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order