proposition: Lemma delta_root_gt m : m < delta (troot m).+1.
proof: Proof. rewrite /troot leqNgt. set l := iota _ _; set f := (fun _ => _). have Hfl : has f l. apply/hasP; exists m.+1; first by rewrite mem_iota leq0n leqnn. rewrite /f /delta -{1}[m.+1](half_bit_double _ false). by apply/half_leq; rewrite add0n -mul2n leq_mul2r orbT. have := nth_find 0 Hfl; rewrite {1}/f. case E : _.-1 => [|n] //. case: find E => // [] [|n] //. by rewrite nth_iota //=; case: (m). rewrite nth_iota. by rewrite -E prednK // ltnNge ltnS. by rewrite -(size_iota 0 m.+2) -has_find. Qed.
imports: mathcomp(all_ssreflect)