proposition: Lemma growing_prop : forall n m:nat, Un_growing -> (n >= m)%nat -> Un n >= Un m.
proof: Proof. intros * Hgrowing Hle. induction Hle as [|p]. - apply Rge_refl. - apply Rge_trans with (Un p). + apply Rle_ge, Hgrowing. + apply IHHle. Qed.
imports: Rbase Rfunctions Compare