proposition: Lemma length_out : forall O E E' A B C D AB CD, A <> B -> C <> D -> Length O E E' A B AB -> Length O E E' C D CD -> Out O AB CD.
proof: Proof. intros. unfold Length in *. spliter. unfold LeP in *. induction H7; induction H4. unfold LtP in *. ex_and H7 X. ex_and H4 Y. apply diff_sum in H7. apply diff_sum in H4. assert(X = AB). apply (sum_uniqueness O E E' O X). apply sum_O_B. unfold Sum in H4. spliter. unfold Ar2 in H4. tauto. unfold Ps in H9. apply out_col in H9. Col. assumption. subst X. assert(Y = CD). apply (sum_uniqueness O E E' O Y). apply sum_O_B. unfold Sum in H4. spliter. unfold Ar2 in H4. tauto. unfold Ps in H10. apply out_col in H10. Col. assumption. subst Y. unfold Ps in *. eapply (l6_7 _ _ E). assumption. apply l6_6. assumption. subst CD. apply cong_symmetry in H5. apply cong_identity in H5. contradiction. subst AB. apply cong_symmetry in H8. apply cong_identity in H8. contradiction. subst CD. apply cong_symmetry in H5. apply cong_identity in H5. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order