proposition: Lemma only_even_fix : forall N n, even n -> only_even n = func_iter N Only_even only_even n.
proof: Proof. Proof using. applys~ (FixFun_fix_partial_iter (@lt nat _)). intros f1 f2 n Pn IH. unfolds. case_if~. case_if. { subst. inverts Pn. } { apply* IH. destruct n as [|[|n']]; tryfalse. simpls. math_rewrite (n'-0=n'). auto. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat