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