proposition: Lemma length_flat_map_le {X: Type} {f g: nat -> list X} {l1 l2: nat} : l1 <= l2 -> (forall i, length (f i) <= length (g i)) -> length (flat_map f (seq 0 l1)) <= length (flat_map g (seq 0 l2)).
proof: Proof. move: (X in (seq X)) => i. move=> + Hfg. elim: l1 l2 i. { move=> /= *. by lia. } move=> l1 IH l2 i ?. have -> : (l2 = S (l2 - 1)) by lia. move=> /=. rewrite ? app_length. have := (IH (l2 - 1) (S i) ltac:(lia)). have := (Hfg i). by lia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM