proposition: Lemma filter_gt_row r n : is_row r -> filter (>%O n) r = take (count (>%O n) r) r.
proof: Proof. Proof using. elim: r => [// | r0 r IHr] Hrow /=. case: (ltP r0 n) => Hr0. - by rewrite add1n (IHr (is_row_consK Hrow)). - rewrite add0n; have Hcount : count (>%O n) r = 0. elim: r r0 Hr0 Hrow {IHr} => [// | r1 r /= IHr] r0 Hr0 /andP[Hr0r1 Hpath]. have Hr1 := le_trans Hr0 Hr0r1. by rewrite ltNge Hr1 (IHr r1 Hr1 Hpath). rewrite Hcount. by apply/nilP; rewrite /nilp size_filter Hcount. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted