proposition: Lemma grow_lft : forall N m : nat, N <= m -> interv_lft (seq1 N) [<=] interv_lft (seq1 m).
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_lft (seq1 m)); auto. astepr (interv_lft (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))). intros. simpl. apply leEq_reflexive. intros. simpl. apply less_leEq. apply less_transitive_unfolded with (lft (interv_lft (seq1 m)) (interv_rht (seq1 m))). apply less_pres_lft. apply interv_lft_rht. apply less_pres_lft_rht. apply interv_lft_rht. Qed.
imports: CoRN.reals.CReals1