proposition: Lemma grow_rht : forall N m : nat, N <= m -> interv_rht (seq1 m) [<=] interv_rht (seq1 N).
proof: Proof. intros. induction m. destruct N; auto. apply leEq_reflexive. assert (S N = 0); auto with arith. elim H0. apply leEq_reflexive. elim H. apply leEq_reflexive. clear IHm. clear H. clear m. intros. apply leEq_transitive with (interv_rht (seq1 m)); auto. astepl (interv_rht (seq_fun (seq1 m) (S m))). unfold seq_fun. case (less_cotransitive_unfolded IR _ _ (less_pres_lft_rht _ _ (interv_lft_rht (seq1 m))) (f (S m))). simpl. intros. apply less_leEq. apply less_transitive_unfolded with (rht (interv_lft (seq1 m)) (interv_rht (seq1 m))). apply less_pres_lft_rht. apply interv_lft_rht. apply less_pres_rht. apply interv_lft_rht. simpl. intros. apply leEq_reflexive. Qed.
imports: CoRN.reals.CReals1