proposition: Lemma eq_size_otake (T : Type) (s1 s2 : seq T) : size s1 = size s2 -> size (otake s1) = size (otake s2).
proof: Proof. by case: s1; case: s2 => //= b s2 a s1 [] /eq_size_etake. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)