The first line is essential, because Litex does not implement transitivity of >= in its kernel and one has to formalize it:
know @larger_equal_is_transitive(x, y, z R):
x >= y
y >= z
For instance, the tutorial says that "The daily properties" (whatever this means) of "+, -, , /, ^, %" are "already in the Litex kernel". What about associativity of and +, or distribution of * over +? Are these part of the "daily properties"? And if so, why didn't transitivity of >= not make the cut?
Just trying to understand the design choices here, this is very interesting.