proposition: Lemma rcons_inj s1 s2 x1 x2 : rcons s1 x1 = rcons s2 x2 :> seq T -> (s1, x1) = (s2, x2).
proof: Proof. by rewrite -!rot1_cons => /rot_inj[-> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)