proposition: Theorem fmap_bound n P : (forall x, x < n -> ex (P x)) -> exists m, forall x, x < n -> exists y, y < m /\ P x y.
proof: Proof. Proof with try lia. revert P; induction n as [ | n IHn ]; intros P HP. + exists 0; intros... + destruct (HP 0) as (m0 & H0)... destruct (IHn (fun n => P (S n))) as (m1 & Hm1). - intros; apply HP... - exists (1+m0+m1); intros [ | x ] Hx. * exists m0; split; auto... * destruct (Hm1 x) as (y & H1 & H2)... exists y; split; auto... Qed.
imports: Arith Lia