proposition: Lemma a_seq_b_seq_dist_n : forall n, b_seq (S n) [-]a_seq (S n) [=] Two [/]ThreeNZ[*] (b_seq n[-]a_seq n).
proof: Proof. intro. unfold a_seq, b_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