proposition: Lemma decreasing_prop : forall (Un:nat -> R) (m n:nat), Un_decreasing Un -> (m <= n)%nat -> Un n <= Un m.
proof: Proof. unfold Un_decreasing; intros. 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 H. -- apply Hrecn; assumption. * rewrite H2; right; reflexivity. + inversion H0; [ right; reflexivity | left; assumption ]. Qed.
imports: Rbase Rfunctions Rseries Lia