proposition: Lemma filter_le_row n r : is_row r -> filter (<=%O n) r = drop (count (>%O n) r) r.
proof: Proof. Proof using. elim: r => //= r0 r IHr Hrow /=. case: (leP n r0) => Hr0. - 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). by rewrite Hcount (IHr (is_row_consK Hrow)) Hcount drop0. - by rewrite add1n (IHr (is_row_consK Hrow)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted