proposition: Lemma remainder_diverges: forall a, diverges (remainder a 0).
proof: Proof. cofix CIH; intros a. unroll_delay (remainder a 0). constructor. apply CIH. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)