This is an alternative to !153 (closed) which follows the spirit of !156 (closed). It is adapted to the last version of coq/coq#12162 which takes into account the introduction of Bool.lt.
Bool.lt