proposition: Lemma finite_seq : forall BOUND t : nat, seq (P BOUND) (fin_is_fin BOUND) t[=]g_ t.
proof: Proof. intros. unfold seq in |- *. unfold fin_is_fin in |- *. unfold Pcard1 in |- *. unfold Pcard1 in |- *. change (g_ t[=]g_ t) in |- *. apply eq_reflexive_unfolded. Qed.
imports: CoRN.reals.Bridges_LUB