proposition: Lemma fin_is_fin : forall BOUND : nat, {n : nat | {r : nat -> OF | forall y : OF, P BOUND y -> {m : nat | m <= n | r m[=]y}}}.
proof: Proof. intros. exists BOUND. exists g_. intros y H. red in H. case H. intro n. intros. exists n. assumption. apply eq_symmetric_unfolded. assumption. Defined.
imports: CoRN.reals.Bridges_LUB