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 n); 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. elim p; clear p; simpl in |- *; intros. elim b2; clear b2; simpl in |- *; auto. Qed.
imports: CoRN.ftc.WeakIVT CoRN.ftc.CalculusTheorems