proposition: Lemma trace_lt_length_filter A n t (LT : NOmega.lt_nat_l n (trace_length t)) (f : A -> Prop) d (F : f (trace_nth n t d)) : NOmega.lt_nat_l (length (filterP f (map (fun i => trace_nth i t d) (List.seq 0 n)))) (trace_length (trace_filter f t)).
proof: Proof. destruct t; ins; desf; ins. erewrite <- map_nth_seq with (a := 0) (l := l) (f := fun i => nth i l d) at 1; auto using app_nth1. rewrite (seq_split0 LT), map_app, filterP_app, length_app; ins; desf; ins; try lia. destruct (IndefiniteDescription.constructive_indefinite_description); ins; desf. specialize (l _ F). rewrite seqS, (seq_split0 l); ins. rewrite !map_app, !filterP_app, !length_app; ins; desf; ins; desf. all: rewrite <- !Nat.add_assoc; apply Nat.lt_add_pos_r; lia. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription