proposition: Lemma filterP_map_seq_eq A (f : A -> Prop) fl a n m (Fn : forall i, f (fl i) -> i < a + n) (Fm : forall i, f (fl i) -> i < a + m) : filterP f (map fl (seq a n)) = filterP f (map fl (seq a m)).
proof: Proof. destruct (lt_eq_lt_dec n m) as [[LT|]|LT]; desf. { rewrite seq_split with (x := n) (y := m); try lia. rewrite map_app, filterP_app. symmetry; rewrite app_eq_prefix, filterP_eq_nil; ins. rewrite in_map_iff in *; desf. rewrite in_seq_iff in *. apply Fn in COND; lia. } { rewrite seq_split with (x := m) (y := n); try lia. rewrite map_app, filterP_app. rewrite app_eq_prefix, filterP_eq_nil; ins. rewrite in_map_iff in *; desf. rewrite in_seq_iff in *. apply Fm in COND; lia. } Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation