Verifying Min-Plus Computations with Coq. - Lucien Rakotomalala; Pierre Roux 001; Marc Boyer (NFM, 2021)