fact: Example p_division (a b : nat) : program (T := unit) unit := p_do _ <- p_put (a, 0); p_while a (fun s => b <= fst s) ( p_do s <- p_get ; p_put (fst s - b, S (snd s)) ).
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model