proposition: Lemma maj_ss : forall (Un:nat -> R) (k:nat), has_ub Un -> has_ub (fun i:nat => Un (k + i)%nat).
proof: Proof. intros. unfold has_ub in H. unfold bound in H. elim H; intros. unfold is_upper_bound in H0. unfold has_ub. exists x. unfold is_upper_bound. intros. apply H0. elim H1; intros. exists (k + x1)%nat; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia