fact: Fixpoint half (n : nat) : nat := if n is n'.+1 then uphalf n' else n with uphalf (n : nat) : nat := if n is n'.+1 then n'./2.+1 else n where "n ./2" := (half n) : nat_scope.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring