proposition: Lemma comp_rseq_limit_compat : forall r env un l, comp_rseq r env = Some un -> comp_limit r env = Some l -> is_limit un l.
proof: Proof. intros r env ; induction r ; intros un l Hun Hl ; simpl in *. inversion Hun ; inversion Hl ; apply Rseq_constant_cv. destruct (nth_error env n) as [Hget |]. inversion Hun ; inversion Hl ; apply (proj2_sig (projT2 Hget)). inversion Hl. destruct (comp_rseq r env) as [vn |] ; [| inversion Hun] ; destruct (comp_limit r env) as [lo |] ; [| inversion Hl] ; inversion Hun ; inversion Hl. apply rseq_limit_opp_is_limit, IHr ; reflexivity. destruct (comp_rseq r1 env) as [vn |] ; [| inversion Hun] ; destruct (comp_limit r1 env) as [ll |] ; [| inversion Hl] ; destruct (comp_rseq r2 env) as [wn |] ; [| inversion Hun] ; destruct (comp_limit r2 env) as [lr |] ; [| inversion Hl]. destruct ll ; destruct lr ; inversion Hun ; inversion Hl ; subst. apply Rseq_cv_neg_infty_plus_compat ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. eapply Rseq_cv_finite_plus_neg_infty_l ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. eapply Rseq_cv_finite_plus_neg_infty_r ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. eapply Rseq_cv_plus_compat ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. eapply Rseq_cv_finite_plus_pos_infty_r ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. eapply Rseq_cv_finite_plus_pos_infty_l ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. apply Rseq_cv_pos_infty_plus_compat ; fold_is_limit ; [apply IHr1 | apply IHr2] ; reflexivity. destruct (comp_rseq r1 env) as [vn |] ; [| inversion Hun] ; destruct (comp_limit r1 env) as [ll |] ; [| inversion Hl] ; destruct (comp_rseq r2 env) as [wn |] ; [| inversion Hun] ; destruct (comp_limit r2 env) as [lr |] ; [| inversion Hl]. inversion Hun ; eapply (is_limit_ext (Rseq_plus vn (Rseq_opp wn))) ; [| intro n ; unfold Rseq_plus, Rseq_minus, Rseq_opp ; ring | reflexivity]. destruct ll ; destruct lr ; inversion Hl ; subst. apply Rseq_cv_finite_plus_neg_infty_l with (- l0)%R ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp (finite l0)) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. apply Rseq_cv_neg_infty_plus_compat ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp plus_inf) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. apply Rseq_cv_finite_plus_pos_infty_r with l0 ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp minus_inf) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. apply Rseq_cv_plus_compat ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp (finite l1)) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. eapply Rseq_cv_finite_plus_neg_infty_r ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp plus_inf) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. apply Rseq_cv_pos_infty_plus_compat ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp minus_inf) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. apply Rseq_cv_finite_plus_pos_infty_l with (- l0)%R ; fold_is_limit ; [apply IHr1 | fold (rseq_limit_opp (finite l0)) ; apply rseq_limit_opp_is_limit, IHr2] ; reflexivity. Qed.
imports: Rbase MyRIneq Rsequence_def Rsequence_facts Rsequence_cv_facts List Option Tactics