proposition: Theorem fmmap_bound p n (P : nat -> (nat -> nat) -> Prop) : (forall x f g, equal_upto p f g -> P x f -> P x g) -> (forall x, x < n -> exists f, P x f) -> exists m, forall x, x < n -> exists f, (forall i, i < p -> f i < m) /\ P x f.
proof: Proof. revert P. induction p as [ | p IHp ]; intros P HP H. + exists 1; intros x Hx. destruct (H _ Hx) as (f & Hf). exists (fun _ => 0); split; auto. apply (HP x f); auto. intros ? ?; lia. + set (Q x y := exists f, P x (fun i => match i with 0 => y | S i => f i end)). destruct (@fmap_bound n Q) as (m1 & Hm1). { intros x Hx. destruct (H _ Hx) as (f & Hf). exists (f 0); red. exists (fun i => f (S i)). revert Hf; apply HP. intros [ | i ]; auto. } set (R x f := exists y, y < m1 /\ P x (fun i => match i with 0 => y | S i => f i end)). destruct (IHp R) as (m2 & Hm2). { intros x f g Hfg (y & H1 & H2); exists y; split; auto. revert H2; apply HP; intros [ | ]; auto; intros; apply Hfg; lia. } { intros x Hx. destruct (Hm1 _ Hx) as (y & H1 & f & H2). exists f, y; split; auto. } exists (m1+m2). intros x Hx. destruct (Hm2 _ Hx) as (f & H1 & y & H2 & H3). eexists; split; [ | exact H3 ]. intros [ | j ] Hj; try lia. specialize (H1 j); intros; lia. Qed.
imports: Arith Lia