proposition: Lemma length_uniqueness : forall O E E' A B AB AB', Length O E E' A B AB -> Length O E E' A B AB' -> AB = AB'.
proof: Proof. intros. assert(Col O E AB /\ ~ Col O E E' \/ AB = O). eapply (length_Ar2 O E E' A B AB); assumption. assert(Col O E AB' /\ ~ Col O E E' \/ AB' = O). eapply (length_Ar2 O E E' A B AB'); assumption. unfold Length in *. spliter. assert(Cong O AB O AB'). apply cong_transitivity with A B; Cong. assert(AB = AB' \/ Midpoint O AB AB'). apply(l7_20 O AB AB'). ColR. Cong. induction H10. assumption. unfold Midpoint in H10. spliter. induction H1; induction H2. spliter. unfold LeP in *. induction H4; induction H7. unfold LtP in H4. unfold LtP in H7. ex_and H4 X. ex_and H7 Y. apply diff_sum in H4. apply diff_sum in H7. assert(X = AB'). apply(sum_O_B_eq O E E'); Col. subst X. assert(Y = AB). apply(sum_O_B_eq O E E'); Col. subst Y. unfold Ps in *. assert(Out O AB AB'). eapply (l6_7 _ _ E). assumption. apply l6_6; assumption. unfold Out in H16. spliter. induction H18. assert(AB = O). eapply (between_equality _ _ AB'); Between. subst AB. apply cong_symmetry in H11. apply cong_identity in H11. auto. assert(AB' = O). eapply (between_equality _ _ AB); Between. subst AB'. apply cong_identity in H11. auto. subst AB. apply cong_symmetry in H9. apply cong_identity in H9. auto. subst AB'. apply cong_identity in H9. auto. subst AB'. apply cong_identity in H9. auto. subst AB'. apply cong_identity in H9. auto. subst AB. apply cong_symmetry in H9. apply cong_identity in H9. auto. subst AB. subst AB'. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order