Comment by litexlang

know @self_defined_axiom_larger_equal_is_transitive(x, y, z R): x >= y y >= z =>: x >= z

Since transitivity of >= is not implemented, one has to call this self_defined_axiom_larger_equal_is_transitive to make x >= 17 here, so

``` know forall x N: x >= 47 => x >= 17 ```

is essential