fact: Definition generic_alpha (i : AQ) : AQ := (cast 17%coqZ * i ^ 2%N + cast 51%coqZ * i + cast 39%coqZ) * (cast 2%coqZ * i + cast 3%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