proposition: Lemma troot_mod_le m n : m <= n = ((troot m < troot n) || ((troot m == troot n) && (tmod m <= tmod n))).
proof: Proof. case: leqP => [|dmGdn] /= ; last first. apply/idP. apply: (leq_trans (_ : _ <= delta (troot m).+1)). by rewrite ltnW // delta_root_gt. apply: (leq_trans (_ : _ <= delta (troot n))). by apply: delta_le. by apply: delta_root_le. rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn]. rewrite dnEdm eqxx /=. by rewrite {1}[m]tmodE {1}[n]tmodE dnEdm leq_add2l. rewrite (gtn_eqF dmLdn) /=. apply/idP/negP. rewrite -ltnNge. apply: (leq_trans (delta_root_gt _)). apply: (leq_trans _ (delta_root_le _)). by apply: delta_le. Qed.
imports: mathcomp(all_ssreflect)