proposition: Theorem iter_until_correct : forall {T} (P : T -> Prop) n step slow_step done, (forall v : T, P v -> P (step v)) -> (forall v : T, P v -> P (slow_step v)) -> forall v : T, P v -> P (iter_until n step slow_step done v).
proof: Proof. intros T P n step slow_step done H Hs. revert slow_step Hs. induction n as [n IH|n IH|] ; intros slow_step Hs v Hv ; simpl. - case done. now apply H. apply H in Hv. apply IH with (1 := Hs) in Hv. case done. exact Hv. apply IH. easy. now apply Hs. - apply IH with (1 := Hs) in Hv. case done. exact Hv. apply IH. easy. now apply Hs. - now apply H. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority