proposition: Lemma sorted_tetake_totake m (t : (m + m).-tuple bool) : sorted <=%O (tetake t) -> sorted <=%O (totake t) -> noF (totake t) <= noF (tetake t) <= (noF (totake t)).+1 -> sorted <=%O t.
proof: Proof. rewrite tetakeE totakeE. move => /isorted_boolP [[a1 a2] teE] /isorted_boolP [[b1 b2] toE] /andP[noFeLnoFo noFoLnoFe]. have : size (tetake t) = size (totake t) by rewrite !size_tuple. move: noFeLnoFo noFoLnoFe. rewrite [X in sorted _ (tval X)]eocat_tetake_totake /= {}teE {}toE !noE. rewrite !(size_cat, size_nseq). case: (ltngtP a1 b1) => // [a1Lb1 | <-] _ b1La1 a1a2E. have b1E : a1 = b1.+1 by case: (ltngtP a1 b1.+1) b1La1 a1Lb1. have ->: b2 = a2.+1 by apply: (@addnI a1); rewrite addnS a1a2E b1E. rewrite b1E; apply/isorted_boolP; exists (b1.*2.+1, a2.*2.+1). by rewrite eocat_nseq_catDS !addnn. have ->: b2 = a2 by apply: (@addnI a1). apply/isorted_boolP; exists (a1.*2, a2.*2). by rewrite eocat_nseq_catD !addnn. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)