proposition: Lemma zero_fix : forall x, zero x = Zero zero x /\ forall x, zero x = 0.
proof: Proof. Proof using. forwards~ [H1 H2]: (FixFun_fix_partial_inv lt pred_true (fun (x y : nat) => y = 0) (F:=Zero)). introv _ H. unfold Zero. case_if~. forwards* [H1 H2]: (H (x-1)). rewrite <- H1. rewrite H2. apply* H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat