for p, q being FinSequence holds
( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p )