Skip to content

Two small lemmas

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

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.

Merge request reports