fact: Definition generic_beta (i : AQ) : AQ := ((i + cast 1%coqZ) %/ (i + cast 2%coqZ)) ^ 3%N.
imports: BinInt mathcomp(all_ssreflect all_algebra) CoqEAL(hrel param refinements) CoqEAL(pos binnat rational) tactics rat_of_Z