proposition: Lemma a_seq_mon : forall i : nat, a_seq i [<=] a_seq (S i).
proof: Proof. intro. unfold a_seq in |- *. simpl in |- *. elim IVT_seq; simpl in |- *; intros. elim IVT_seq_lemma; simpl in |- *; intro. elim x; simpl in |- *; clear x; intros. elim p; clear p; intro. elim x; simpl in |- *; clear x; intros. case q; clear q; simpl in |- *; intros. case a2; clear a2; simpl in |- *; intros. case a2; clear a2; simpl in |- *; intros. case a2; auto. Qed.
imports: CoRN.ftc.Continuity