Two small lemmas (!107) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis · GitLab

Pierre Roux requested to merge proux/rt-proofs:nccoq-prosa-missing into master Aug 27, 2020

These are two lemmas that were needed when digging up the link between Prosa and Network Calculus (c.f., https://gitlab.mpi-sws.org/RT-PROOFS/project-administration/-/issues/23) and are currently in my prosa_missing directory https://gitlab.mpi-sws.org/proux/nc-coq/-/tree/prosa-link/prosa_missing . I don't know if we want to integrate them into Prosa.