proposition: Lemma root_delta_le m n : (n <= troot m) = (delta n <= m).
proof: Proof. case: leqP => [/delta_le/leq_trans->//|dmLn]. apply: delta_root_le. apply/sym_equal/idP/negP. rewrite -ltnNge. by apply: leq_trans (delta_root_gt _) (delta_le dmLn). Qed.
imports: mathcomp(all_ssreflect)