proposition: Lemma a'_seq_b'_seq_dist : forall n, b'_seq n[-]a'_seq n [=] (Two [/]ThreeNZ) [^]n[*] (b[-]a).
proof: Proof. simple induction n. simpl in |- *; algebra. clear n; intros. astepr (Two [/]ThreeNZ[*] (Two [/]ThreeNZ) [^]n[*] (b[-]a)). astepr (Two [/]ThreeNZ[*] ((Two [/]ThreeNZ) [^]n[*] (b[-]a))). astepr (Two [/]ThreeNZ[*] (b'_seq n[-]a'_seq n)). apply a'_seq_b'_seq_dist_n. Qed.
imports: CoRN.ftc.WeakIVT CoRN.ftc.CalculusTheorems