Thank you @Huỳnh Trần Khanh for the nice trick (and the cool interpretation of the second variable as fuel).
Thank you @Guillaume Melquiond for the explanation. Maybe it could be possible to let
n0 appear in the definition, as printed by coq (it's already different from what I wrote) ?
Pierre Rousselin has marked this topic as resolved.
Last updated: Feb 08 2023 at 23:03 UTC