Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
1022 commits behind the upstream repository.
-
Felipe Cerqueira authoredFelipe Cerqueira authored
divround.v 164 B
Require Import Vbase ssrbool ssrnat div.
Definition div_floor (x y: nat) : nat := x %/ y.
Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.