feat(builtin): prove strong induction theorem, add < theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/Nat.lean

@@ -21,10 +21,10 @@ definition ge (a b : Nat) := b ≤ a
 infix 50 >= : ge
 infix 50 ≥  : ge
 
-definition lt (a b : Nat) := ¬ (a ≥ b)
+definition lt (a b : Nat) := a + 1 ≤ b
 infix 50 <  : lt
 
-definition gt (a b : Nat) := ¬ (a ≤ b)
+definition gt (a b : Nat) := b < a
 infix 50 >  : gt
 
 definition id (a : Nat) := a
@@ -37,10 +37,13 @@ axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
 axiom mul_zeror (a : Nat)    : a * 0 = 0
 axiom mul_succr (a b : Nat)  : a * (b + 1) = a * b + a
 axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b
-axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
+axiom induction {P : Nat → Bool} (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : ∀ a, P a
+
+theorem induction_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
+:= induction H1 H2 a
 
 theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
-:= induction a
+:= induction_on a
     (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H)
     (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
        or_elim (em (n = 0))
@@ -56,14 +59,14 @@ theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n +
                   H2 w (symm Hw))
 
 theorem add_zerol (a : Nat) : 0 + a = a
-:= induction a
+:= induction_on a
     (have 0 + 0 = 0 : trivial)
     (λ (n : Nat) (iH : 0 + n = n),
         calc  0 + (n + 1)  =  (0 + n) + 1   :  add_succr 0 n
                     ...    =  n + 1         :  { iH })
 
 theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
-:= induction b
+:= induction_on b
     (calc (a + 1) + 0   =  a + 1        :  add_zeror (a + 1)
                   ...   =  (a + 0) + 1  :  { symm (add_zeror a) })
     (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
@@ -72,7 +75,7 @@ theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
                               ...  =   (a + (n + 1)) + 1  :  { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) })
 
 theorem add_comm (a b : Nat) : a + b = b + a
-:= induction b
+:= induction_on b
     (calc a + 0   = a     : add_zeror a
             ...   = 0 + a : symm (add_zerol a))
     (λ (n : Nat) (iH : a + n = n + a),
@@ -81,7 +84,7 @@ theorem add_comm (a b : Nat) : a + b = b + a
                        ...   =   (n + 1) + a : symm (add_succl n a))
 
 theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
-:= induction a
+:= induction_on a
     (calc 0 + (b + c)  =  b + c        : add_zerol (b + c)
                   ...  =  (0 + b) + c  : { symm (add_zerol b) })
     (λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
@@ -91,7 +94,7 @@ theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
                           ...    =    ((n + 1) + b) + c   :  { have (n + b) + 1 = (n + 1) + b :  symm (add_succl n b) })
 
 theorem mul_zerol (a : Nat) : 0 * a = 0
-:= induction a
+:= induction_on a
     (have 0 * 0 = 0 : trivial)
     (λ (n : Nat) (iH : 0 * n = 0),
         calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
@@ -99,7 +102,7 @@ theorem mul_zerol (a : Nat) : 0 * a = 0
                       ...  =  0           : trivial)
 
 theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
-:= induction b
+:= induction_on b
     (calc (a + 1) * 0   =  0         : mul_zeror (a + 1)
                    ...  =  a * 0     : symm (mul_zeror a)
                    ...  =  a * 0 + 0 : symm (add_zeror (a * 0)))
@@ -114,21 +117,21 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
                             ...   = a * (n + 1) + (n + 1)     :  symm (add_assoc (a * (n + 1)) n 1))
 
 theorem mul_onel (a : Nat) : 1 * a = a
-:= induction a
+:= induction_on a
     (have 1 * 0 = 0 : trivial)
     (λ (n : Nat) (iH : 1 * n = n),
         calc  1 * (n + 1)  =  1 * n + 1 :  mul_succr 1 n
                       ...  =  n + 1     : { iH })
 
 theorem mul_oner (a : Nat) : a * 1 = a
-:= induction a
+:= induction_on a
     (have 0 * 1 = 0 : trivial)
     (λ (n : Nat) (iH : n * 1 = n),
         calc  (n + 1) * 1  =  n * 1 + 1 : mul_succl n 1
                       ...  =  n + 1     : { iH })
 
 theorem mul_comm (a b : Nat) : a * b = b * a
-:= induction b
+:= induction_on b
     (calc a * 0  = 0      : mul_zeror a
             ...  = 0 * a  : symm (mul_zerol a))
     (λ (n : Nat) (iH : a * n = n * a),
@@ -137,7 +140,7 @@ theorem mul_comm (a b : Nat) : a * b = b * a
                        ...   =   (n + 1) * a : symm (mul_succl n a))
 
 theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c
-:= induction a
+:= induction_on a
     (calc 0 * (b + c)   = 0              : mul_zerol (b + c)
                   ...   = 0 + 0          : trivial
                   ...   = 0 * b + 0      : { symm (mul_zerol b) }
@@ -160,7 +163,7 @@ theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c
                 ...  =  a * c + b * c  :  { mul_comm c b }
 
 theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c
-:= induction a
+:= induction_on a
     (calc  0 * (b * c)    =  0           : mul_zerol (b * c)
                    ...    =  0 * c       : symm (mul_zerol c)
                    ...    =  (0 * b) * c : { symm (mul_zerol b) })
@@ -170,8 +173,8 @@ theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c
                             ...    =   (n * b + b) * c         :  symm (distributel (n * b) b c)
                             ...    =   (n + 1) * b * c         :  { symm (mul_succl n b) })
 
-theorem add_inj {a b c : Nat} : a + b = a + c → b = c
+theorem add_injr {a b c : Nat} : a + b = a + c → b = c
-:= induction a
+:= induction_on a
     (λ H : 0 + b = 0 + c,
         calc b   =  0 + b   : symm (add_zerol b)
            ...   =  0 + c   : H
@@ -188,6 +191,11 @@ theorem add_inj {a b c : Nat} : a + b = a + c → b = c
            L2 : n + b = n + c := succ_inj L1
        in iH L2)
 
+theorem add_injl {a b c : Nat} (H : a + b = c + b) : a = c
+:= add_injr (calc b + a  =  a + b  : add_comm _ _
+                   ...   =  c + b  : H
+                   ...   =  b + c  : add_comm _ _)
+
 theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0
 := discriminate
      (λ H1 : a = 0, H1)
@@ -228,7 +236,7 @@ theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
 := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
    obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2),
     let L1 : w1 + w2 = 0
-           := add_inj (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 }
+           := add_injr (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 }
                                        ... = b + w2        : { Hw1 }
                                        ... = a             : Hw2
                                        ... = a + 0         : symm (add_zeror a)),
@@ -237,6 +245,104 @@ theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
           ...  =  a  + w1 : { symm L2 }
           ...  =  b       : Hw1
 
+theorem not_lt_0 (a : Nat) : ¬ a < 0
+:= not_intro (λ H : a + 1 ≤ 0,
+               obtain (w : Nat) (Hw1 : a + 1 + w = 0), from (le_elim H),
+                  absurd
+                    (calc a + w + 1  =  a + (w + 1)  : symm (add_assoc _ _ _)
+                                ...  =  a + (1 + w)  : { add_comm _ _ }
+                                ...  =  a + 1 + w    : add_assoc _ _ _
+                                ...  =  0            : Hw1)
+                    (succ_nz (a + w)))
+
+theorem lt_intro {a b c : Nat} (H : a + 1 + c = b) : a < b
+:= le_intro H
+
+theorem lt_elim {a b : Nat} (H : a < b) : ∃ x, a + 1 + x = b
+:= le_elim H
+
+theorem lt_le {a b : Nat} (H : a < b) : a ≤ b
+:= obtain (w : Nat) (Hw : a + 1 + w = b), from (le_elim H),
+     le_intro (calc a + (1 + w) =  a + 1 + w  :  add_assoc _ _ _
+                            ... =  b          : Hw)
+
+theorem lt_ne {a b : Nat} (H : a < b) : a ≠ b
+:= not_intro (λ H1 : a = b,
+      obtain (w : Nat) (Hw : a + 1 + w = b), from (lt_elim H),
+          absurd (calc w + 1 = 1 + w     : add_comm _ _
+                        ...  = 0         :
+                               add_injr (calc b + (1 + w)  = b + 1 + w   : add_assoc b 1 w
+                                                    ...    = a + 1 + w   : { symm H1 }
+                                                    ...    =  b          : Hw
+                                                    ...    =  b + 0      : symm (add_zeror b)))
+                 (succ_nz w))
+
+theorem lt_nrefl (a : Nat) : ¬ a < a
+:= not_intro (λ H : a < a,
+      absurd (refl a) (lt_ne H))
+
+theorem lt_trans {a b c : Nat} (H1 : a < b) (H2 : b < c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
+      lt_intro (calc a + 1 + (w1 + 1 + w2) = a + 1 + (w1 + (1 + w2))   : { symm (add_assoc w1 1 w2) }
+                                       ... = (a + 1 + w1) + (1 + w2)   : add_assoc _ _ _
+                                       ... =  b + (1 + w2)             :  { Hw1 }
+                                       ... =  b + 1 + w2               : add_assoc _ _ _
+                                       ... =  c                        :  Hw2)
+
+theorem lt_le_trans {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + 1 + w1 = b), from (lt_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
+      lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2   : add_assoc _ _ _
+                                   ... =  b + w2             :  { Hw1 }
+                                   ... =  c                  :  Hw2)
+
+theorem le_lt_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b < c) : a < c
+:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
+   obtain (w2 : Nat) (Hw2 : b + 1 + w2 = c), from (lt_elim H2),
+      lt_intro (calc a + 1 + (w1 + w2) = a + 1 + w1 + w2   : add_assoc _ _ _
+                                   ... = a + (1 + w1) + w2 : { symm (add_assoc a 1 w1) }
+                                   ... = a + (w1 + 1) + w2 : { add_comm 1 w1 }
+                                   ... = a + w1 + 1 + w2   : { add_assoc a w1 1 }
+                                   ... = b + 1 + w2        : { Hw1 }
+                                   ... = c                 : Hw2)
+
+theorem ne_lt_succ {a b : Nat} (H1 : a ≠ b) (H2 : a < b + 1) : a < b
+:= obtain (w : Nat) (Hw : a + 1 + w = b + 1), from (lt_elim H2),
+     let L : a + w = b := add_injl (calc a + w + 1  =  a + (w + 1)  : symm (add_assoc _ _ _)
+                                                ... =  a + (1 + w)  : { add_comm _ _ }
+                                                ... =  a + 1 + w    : add_assoc _ _ _
+                                                ... =  b + 1        : Hw)
+     in discriminate (λ Hz : w = 0, absurd_elim (a < b) (calc a   = a + 0  : symm (add_zeror _)
+                                                              ... = a + w  : { symm Hz }
+                                                              ... = b      : L)
+                                                         H1)
+                     (λ (p : Nat) (Hp : w = p + 1), lt_intro (calc a + 1 + p =  a + (1 + p)   : symm (add_assoc _ _ _)
+                                                                        ...  =  a + (p + 1)   : { add_comm _ _ }
+                                                                        ...  =  a + w         : { symm Hp }
+                                                                        ...  =  b             : L))
+
+theorem strong_induction {P : Nat → Bool} (H : ∀ n, (∀ m, m < n → P m) → P n) : ∀ a, P a
+:= λ a,
+    let stronger : P a ∧ ∀ m, m < a → P m :=
+      -- we prove a stronger result by regular induction on a
+      induction_on a
+        (have P 0 ∧ ∀ m, m < 0 → P m :
+            let c2 : ∀ m, m < 0 → P m := λ (m : Nat) (Hlt : m < 0), absurd_elim (P m) Hlt (not_lt_0 m),
+                c1 : P 0                := H 0 c2
+            in and_intro c1 c2)
+        (λ (n : Nat) (iH : P n ∧ ∀ m, m < n → P m),
+            have P (n + 1) ∧ ∀ m, m < n + 1 → P m :
+              let iH1 : P n                    := and_eliml iH,
+                  iH2 : ∀ m, m < n → P m     := and_elimr iH,
+                  c2  : ∀ m, m < n + 1 → P m := λ (m : Nat) (Hlt : m < n + 1),
+                                                    or_elim (em (m = n))
+                                                      (λ Heq : m = n, subst iH1 (symm Heq))
+                                                      (λ Hne : m ≠ n, iH2 m (ne_lt_succ Hne Hlt)),
+                  c1  : P (n + 1)              := H (n + 1) c2
+              in and_intro c1 c2)
+    in and_eliml stronger
+
 set_opaque add true
 set_opaque mul true
 set_opaque le true

src/builtin/kernel.lean

@@ -64,6 +64,10 @@ axiom allext {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀
 theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
 := subst H1 H2
 
+-- We will mark not as opaque later
+theorem not_intro {a : Bool} (H : a → false) : ¬ a
+:= H
+
 theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
 := funext (λ x : A, refl (f x))
 

src/kernel/kernel_decls.cpp

@@ -22,6 +22,7 @@ MK_CONSTANT(subst_fn, name("subst"));
 MK_CONSTANT(funext_fn, name("funext"));
 MK_CONSTANT(allext_fn, name("allext"));
 MK_CONSTANT(substp_fn, name("substp"));
+MK_CONSTANT(not_intro_fn, name("not_intro"));
 MK_CONSTANT(eta_fn, name("eta"));
 MK_CONSTANT(trivial, name("trivial"));
 MK_CONSTANT(absurd_fn, name("absurd"));

src/kernel/kernel_decls.h

@@ -58,6 +58,9 @@ inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr
 expr mk_substp_fn();
 bool is_substp_fn(expr const & e);
 inline expr mk_substp_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_substp_fn(), e1, e2, e3, e4, e5, e6}); }
+expr mk_not_intro_fn();
+bool is_not_intro_fn(expr const & e);
+inline expr mk_not_intro_th(expr const & e1, expr const & e2) { return mk_app({mk_not_intro_fn(), e1, e2}); }
 expr mk_eta_fn();
 bool is_eta_fn(expr const & e);
 inline expr mk_eta_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eta_fn(), e1, e2, e3}); }

src/library/arith/Nat_decls.cpp

@@ -19,6 +19,7 @@ MK_CONSTANT(Nat_mul_zeror_fn, name({"Nat", "mul_zeror"}));
 MK_CONSTANT(Nat_mul_succr_fn, name({"Nat", "mul_succr"}));
 MK_CONSTANT(Nat_le_def_fn, name({"Nat", "le_def"}));
 MK_CONSTANT(Nat_induction_fn, name({"Nat", "induction"}));
+MK_CONSTANT(Nat_induction_on_fn, name({"Nat", "induction_on"}));
 MK_CONSTANT(Nat_pred_nz_fn, name({"Nat", "pred_nz"}));
 MK_CONSTANT(Nat_discriminate_fn, name({"Nat", "discriminate"}));
 MK_CONSTANT(Nat_add_zerol_fn, name({"Nat", "add_zerol"}));
@@ -33,7 +34,8 @@ MK_CONSTANT(Nat_mul_comm_fn, name({"Nat", "mul_comm"}));
 MK_CONSTANT(Nat_distributer_fn, name({"Nat", "distributer"}));
 MK_CONSTANT(Nat_distributel_fn, name({"Nat", "distributel"}));
 MK_CONSTANT(Nat_mul_assoc_fn, name({"Nat", "mul_assoc"}));
-MK_CONSTANT(Nat_add_inj_fn, name({"Nat", "add_inj"}));
+MK_CONSTANT(Nat_add_injr_fn, name({"Nat", "add_injr"}));
+MK_CONSTANT(Nat_add_injl_fn, name({"Nat", "add_injl"}));
 MK_CONSTANT(Nat_add_eqz_fn, name({"Nat", "add_eqz"}));
 MK_CONSTANT(Nat_le_intro_fn, name({"Nat", "le_intro"}));
 MK_CONSTANT(Nat_le_elim_fn, name({"Nat", "le_elim"}));
@@ -42,4 +44,15 @@ MK_CONSTANT(Nat_le_zero_fn, name({"Nat", "le_zero"}));
 MK_CONSTANT(Nat_le_trans_fn, name({"Nat", "le_trans"}));
 MK_CONSTANT(Nat_le_add_fn, name({"Nat", "le_add"}));
 MK_CONSTANT(Nat_le_antisym_fn, name({"Nat", "le_antisym"}));
+MK_CONSTANT(Nat_not_lt_0_fn, name({"Nat", "not_lt_0"}));
+MK_CONSTANT(Nat_lt_intro_fn, name({"Nat", "lt_intro"}));
+MK_CONSTANT(Nat_lt_elim_fn, name({"Nat", "lt_elim"}));
+MK_CONSTANT(Nat_lt_le_fn, name({"Nat", "lt_le"}));
+MK_CONSTANT(Nat_lt_ne_fn, name({"Nat", "lt_ne"}));
+MK_CONSTANT(Nat_lt_nrefl_fn, name({"Nat", "lt_nrefl"}));
+MK_CONSTANT(Nat_lt_trans_fn, name({"Nat", "lt_trans"}));
+MK_CONSTANT(Nat_lt_le_trans_fn, name({"Nat", "lt_le_trans"}));
+MK_CONSTANT(Nat_le_lt_trans_fn, name({"Nat", "le_lt_trans"}));
+MK_CONSTANT(Nat_ne_lt_succ_fn, name({"Nat", "ne_lt_succ"}));
+MK_CONSTANT(Nat_strong_induction_fn, name({"Nat", "strong_induction"}));
 }

src/library/arith/Nat_decls.h

@@ -47,6 +47,9 @@ inline expr mk_Nat_le_def_th(expr const & e1, expr const & e2) { return mk_app({
 expr mk_Nat_induction_fn();
 bool is_Nat_induction_fn(expr const & e);
 inline expr mk_Nat_induction_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_induction_on_fn();
+bool is_Nat_induction_on_fn(expr const & e);
+inline expr mk_Nat_induction_on_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_induction_on_fn(), e1, e2, e3, e4}); }
 expr mk_Nat_pred_nz_fn();
 bool is_Nat_pred_nz_fn(expr const & e);
 inline expr mk_Nat_pred_nz_th(expr const & e1, expr const & e2) { return mk_app({mk_Nat_pred_nz_fn(), e1, e2}); }
@@ -89,9 +92,12 @@ inline expr mk_Nat_distributel_th(expr const & e1, expr const & e2, expr const &
 expr mk_Nat_mul_assoc_fn();
 bool is_Nat_mul_assoc_fn(expr const & e);
 inline expr mk_Nat_mul_assoc_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_mul_assoc_fn(), e1, e2, e3}); }
-expr mk_Nat_add_inj_fn();
+expr mk_Nat_add_injr_fn();
-bool is_Nat_add_inj_fn(expr const & e);
+bool is_Nat_add_injr_fn(expr const & e);
-inline expr mk_Nat_add_inj_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_inj_fn(), e1, e2, e3, e4}); }
+inline expr mk_Nat_add_injr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injr_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_add_injl_fn();
+bool is_Nat_add_injl_fn(expr const & e);
+inline expr mk_Nat_add_injl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_add_injl_fn(), e1, e2, e3, e4}); }
 expr mk_Nat_add_eqz_fn();
 bool is_Nat_add_eqz_fn(expr const & e);
 inline expr mk_Nat_add_eqz_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_add_eqz_fn(), e1, e2, e3}); }
@@ -116,4 +122,37 @@ inline expr mk_Nat_le_add_th(expr const & e1, expr const & e2, expr const & e3,
 expr mk_Nat_le_antisym_fn();
 bool is_Nat_le_antisym_fn(expr const & e);
 inline expr mk_Nat_le_antisym_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_le_antisym_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_not_lt_0_fn();
+bool is_Nat_not_lt_0_fn(expr const & e);
+inline expr mk_Nat_not_lt_0_th(expr const & e1) { return mk_app({mk_Nat_not_lt_0_fn(), e1}); }
+expr mk_Nat_lt_intro_fn();
+bool is_Nat_lt_intro_fn(expr const & e);
+inline expr mk_Nat_lt_intro_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_lt_intro_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_lt_elim_fn();
+bool is_Nat_lt_elim_fn(expr const & e);
+inline expr mk_Nat_lt_elim_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_elim_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_le_fn();
+bool is_Nat_lt_le_fn(expr const & e);
+inline expr mk_Nat_lt_le_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_le_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_ne_fn();
+bool is_Nat_lt_ne_fn(expr const & e);
+inline expr mk_Nat_lt_ne_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_lt_ne_fn(), e1, e2, e3}); }
+expr mk_Nat_lt_nrefl_fn();
+bool is_Nat_lt_nrefl_fn(expr const & e);
+inline expr mk_Nat_lt_nrefl_th(expr const & e1) { return mk_app({mk_Nat_lt_nrefl_fn(), e1}); }
+expr mk_Nat_lt_trans_fn();
+bool is_Nat_lt_trans_fn(expr const & e);
+inline expr mk_Nat_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_lt_le_trans_fn();
+bool is_Nat_lt_le_trans_fn(expr const & e);
+inline expr mk_Nat_lt_le_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_lt_le_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_le_lt_trans_fn();
+bool is_Nat_le_lt_trans_fn(expr const & e);
+inline expr mk_Nat_le_lt_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_Nat_le_lt_trans_fn(), e1, e2, e3, e4, e5}); }
+expr mk_Nat_ne_lt_succ_fn();
+bool is_Nat_ne_lt_succ_fn(expr const & e);
+inline expr mk_Nat_ne_lt_succ_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_Nat_ne_lt_succ_fn(), e1, e2, e3, e4}); }
+expr mk_Nat_strong_induction_fn();
+bool is_Nat_strong_induction_fn(expr const & e);
+inline expr mk_Nat_strong_induction_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_Nat_strong_induction_fn(), e1, e2, e3}); }
 }