proposition: Lemma troot_mod_case m : ((troot m.+1 == troot m) && (tmod m.+1 == (tmod m).+1)) || [&& troot m.+1 == (troot m).+1, tmod m.+1 == 0 & tmod m == troot m].
proof: Proof. have := troot_le (leqnSn m). rewrite leq_eqVlt => /orP[/eqP He|He]. by rewrite /tmod -He subSn ?eqxx // {2}[m]tmodE leq_addr. rewrite orbC. have: troot m.+1 == (troot m).+1. rewrite trootE (leq_trans (delta_le He)) //; last first. by rewrite {2}[m.+1]tmodE leq_addr. rewrite !deltaS {1}[m]tmodE -addnS -addnS -addnA. by rewrite leq_add2l (leq_trans _ (leq_addl _ _)) // !ltnS tmod_le. move/eqP=> He1. rewrite He1 eqxx. have := eqxx m.+1. rewrite {1}[m]tmodE {1}[m.+1]tmodE He1 deltaS -addnS. rewrite -!addnA eqn_add2l addSn eqSS => /eqP He2. have := tmod_le m. rewrite leq_eqVlt => /orP[/eqP He3|]; last first. by rewrite He2 ltnNge leq_addr. rewrite He3 -(eqn_add2l (tmod m)) {1}He3 -He2 addn0. by rewrite !eqxx. Qed.
imports: mathcomp(all_ssreflect)