proposition: Lemma tnth_lshift i : tnth [tuple of t1 ++ t2] (lshift n2 i) = tnth t1 i.
proof: Proof. have x0 := tnth_default t1 i; rewrite !(tnth_nth x0). by rewrite nth_cat size_tuple /= ltn_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)