proposition: Lemma iter_down_sound: forall n S, ST.le (F S) S -> ST.le (F (iter_down n S)) (iter_down n S).
proof: Proof. induction n; intros; cbn. - auto. - destruct (ST.ble (F (F S)) (F S)) eqn:BLE. + apply IHn. apply ST.ble_1; auto. + auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)