proposition: Lemma rot_rot_add n m s : rot m (rot n s) = rot (rot_add s n m) s.
proof: Proof. unlock rot_add. by rewrite (rot_minn n) (rot_minn m) rot_add_mod ?size_rot ?geq_minr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)