Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.