fact: Definition Rbool := fun_hrel F2_of_bool.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div choice) mathcomp(fintype bigop finset prime fingroup ssralg zmodp finalg) CoqEAL(hrel param refinements)