proposition: Lemma tech9 : forall Un:nat -> R, Un_growing Un -> forall m n:nat, (m <= n)%nat -> Un m <= Un n.
proof: Proof. intros; unfold Un_growing in H. induction n as [| n Hrecn]. - induction m as [| m Hrecm]. + right; reflexivity. + elim (Nat.nle_succ_0 _ H0). - cut ((m <= n)%nat \/ m = S n). + intro; elim H1; intro. * apply Rle_trans with (Un n). -- apply Hrecn; assumption. -- apply H. * rewrite H2; right; reflexivity. + inversion H0. * right; reflexivity. * left; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia