fact: Fixpoint fib (n : nat) : nat := match n with | 0 => 1 | 1 => 1 | (m.+1 as sm).+1 => fib sm + fib m end.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer