fact: Definition F2_of_bool (x : bool) : 'F_2 := x%:R.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div choice) mathcomp(fintype bigop finset prime fingroup ssralg zmodp finalg) CoqEAL(hrel param refinements)