fact: Definition archi_boundP x : 0 <= x -> x < (bound x)%:R := @ssrnum.Num.Theory.mc_2_0.archi_boundP R x.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)