StreamCalculus.streamscommon

Definition nat_lt := lt.

Require Import MathClasses.interfaces.abstract_algebra.
Set Implicit Arguments.

Section Streams.
  Context (R: Type).
  Definition Stream:=nat -> R.
  Definition derive (s:Stream):Stream:=fun n=>s (S n).

  Lemma derive_rewrite (s1: Stream) n:
    eq (s1 (S n)) (derive s1 n).
  Proof.
    trivial.
  Qed.
End Streams.

Section CommonLemma.
  Variable (T: Type).
  Context `{R: Ring T}.
  Lemma minus_0:
    - 0 = 0.
  Proof.
    assert (Azero - Azero = Azero).
    { now rewrite right_inverse. }
    now rewrite left_identity in H.
  Qed.
End CommonLemma.