proposition: Lemma McCarthy_spec_gt100 : forall n, n > 100 -> mcCarthy n = n - 10.
proof: Proof. Proof using. introv Lt. lets H: (proj2 McCarthy_fix_post n). unfolds in H. case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat