Verify lemmas in TODO in π§ββοΈ Test_sc_rollup_tick_repr.v
In https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt_generated/test_sc_rollup_tick_repr verify the following lemmas, left in "TODO":
-
test_distance_triangle_inequality_proof
-
test_of_int_to_int_proof
Edited by Guillaume Claret