proposition: Theorem fmap_reifer_bound n P : (forall x, x < n -> ex (P x)) -> exists m f, forall x, x < n -> f x < m /\ P x (f x).
proof: Proof. intros H. apply fmap_bound in H. destruct H as (m & Hm); exists m. revert Hm; apply fmap_reifier_default; auto. Qed.
imports: Arith Lia