proposition: Lemma delta_root_le m : delta (troot m) <= m.
proof: Proof. rewrite /troot leqNgt. set l := iota _ _; set f := (fun _ => _). case E : _.-1 => [|n] //. have /(before_find 0) : (find f l).-1 < find f l by rewrite prednK // E. rewrite E nth_iota // /f => [->//|]. rewrite -[m.+2](size_iota 0) -E prednK; first by apply: find_size. by case: find E. Qed.
imports: mathcomp(all_ssreflect)