noetherian-implies-streamless We provide two Coq proofs that noetherian implies streamless, one proof uses equality, the other is expressible withouth equality.