for k, n being Nat holds Seg k, Seg n are_c=-comparable