% There is no path of length < (N-1)+(N-2) leading to the situation % where all girls know all gossips (true) nu X(n:Nat = 0) . val(n < (N-1)+(N-2)) => ([true] X(n+1) && [all_done] false)