proposition: Lemma McCarthy_spec_le100 : forall n, n <= 100 -> mcCarthy n = 91.
proof: Proof. Proof using. introv Le. 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