LittleJianCH

#lang racket

(require "Racket-miniKanren/minikanren/mk.rkt")

(defrel (conso a d p)
  (== (cons a d) p))

(defrel (caro p a)
  (fresh (d)
    (conso a d p)))

LittleJianCH

Require Import Coq.Arith.PeanoNat.
Require Import Lia.

Theorem lemma1 : forall (n : nat),
  4 <= n ->
  2 * n + 1 <= 2 ^ n.
Proof.
  intros n Hle.
  induction Hle.
  - simpl. lia.

LittleJianCH

#lang pie

(define destruct-Nat-with-eq
  (λ (n motive motive0 motiveM)
    ((ind-Nat n
       (λ (k) (→ (= Nat k n) (motive k)))
       (λ (_) motive0)
       (λ (n-1 useless eq)
         (motiveM n-1 eq)))
     (same n))))