proposition: Lemma tnth_rshift j : tnth [tuple of t1 ++ t2] (rshift n1 j) = tnth t2 j.
proof: Proof. have x0 := tnth_default t2 j; rewrite !(tnth_nth x0). by rewrite nth_cat size_tuple ltnNge leq_addr /= addKn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)