List of avaCorrect Lean 4.20 API for Natural ilable theorems

Stream: new members

[Harikrishnan R]

QUESTION: Correct Lean 4.20 API for Natural Number Multiplication Inequality

Context: UYA Theory Chapter 1 - Vedic Algorithm Termination Proofs
Date: 2025-08-04
Lean Version: 4.20.0

Problem Summary:
We need to prove k * q > k given k > 1 and q > 1 for a Vedic algorithm termination proof, but multiple Nat API functions we've tried don't exist or have wrong signatures in Lean 4.20. We need guidance on the correct Lean 4.20 API for this type of multiplication inequality proof.

Background Context:
This is part of a drop lemma for proving WellFounded termination using the Robin Arnez/Aaron Liu pattern with Subrelation.wf. The mathematical reasoning is sound: k > 1 and q > 1 implies k * q > k * 1 = k. We just need the correct Lean 4.20 API to express this.

MWE (Minimal Working Example):

-- MWE: Natural Number API Issue for Anurupyena Drop Lemma
import Std.Data.Nat.Basic

-- FAILED API ATTEMPTS (these don't work in Lean 4.20):

example (k q : ℕ) (hk_gt : k > 1) (hq_gt : q > 1) : k * q > k := by
  have h_k_pos : 0 < k := Nat.zero_lt_of_lt hk_gt
  -- ATTEMPT 1: This constant doesn't exist
  -- exact Nat.lt_mul_of_one_lt_right h_k_pos hq_gt  -- unknown constant
  sorry

example (k q : ℕ) (hk_gt : k > 1) (hq_gt : q > 1) : k * q > k := by
  have h_k_pos : 0 < k := Nat.zero_lt_of_lt hk_gt
  -- ATTEMPT 2: This returns biconditional, causes type mismatch
  rw [← Nat.mul_one k]
  -- exact (Nat.mul_lt_mul_left h_k_pos).mpr hq_gt  -- type mismatch
  sorry

-- WORKING CONTEXT: This proof is needed in the following drop lemma pattern:

inductive Anurupyena : ℕ × ℕ → ℕ × ℕ → Prop
| step {p q} (hp_pos : 0 < p) (hq_gt : q > 1) (h_factor : ∃ k > 1, p = k * q) :
    Anurupyena (p, q) (p / q, q)

private lemma anurupyena_drop : ∀ {p q}, Anurupyena p q → p.1 > q.1 := by
  intro ⟨p, q⟩ ⟨p', q'⟩ h
  cases h with
  | step hp_pos hq_gt h_factor =>
    simp only [Prod.fst]
    obtain ⟨k, hk_gt, hk_eq⟩ := h_factor
    rw [hk_eq]
    have h_div_eq : k * q / q = k := Nat.mul_div_cancel k (Nat.zero_lt_of_lt hq_gt)
    rw [h_div_eq]
    -- HERE IS WHERE WE NEED: k * q > k given k > 1, q > 1
    -- What is the correct Lean 4.20 API for this?
    have h_k_pos : 0 < k := Nat.zero_lt_of_lt hk_gt
    -- NEED HELP HERE: correct API to prove k * q > k
    sorry

theorem anurupyena_terminates : WellFounded (fun a b => Anurupyena b a) := by
  have wf_fst : WellFounded (fun p q : ℕ × ℕ ↦ p.1 < q.1) := by
    exact InvImage.wf (fun p : ℕ × ℕ => p.1) wellFounded_lt
  exact Subrelation.wf anurupyena_drop wf_fst

Specific Questions:

Q1: What is the correct Lean 4.20 API to prove k * q > k given k > 1 and q > 1?

Q2: We've seen references to functions like:

• Nat.lt_mul_of_one_lt_right (doesn't exist)
• Nat.mul_lt_mul_left (returns biconditional, not direct proof)
  What are the correct function names and usage patterns?

Q3: Is there a systematic way to find these multiplication inequality lemmas? We've tried searching mathlib docs but the naming conventions are unclear.

What We've Tried:

1. Nat.lt_mul_of_one_lt_right (unknown constant)
2. Nat.mul_lt_mul_left with .mpr (type mismatch after rewrite)
3. Various combinations with Nat.mul_one, rewrites, etc.
4. Searching mathlib documentation (naming conventions unclear)

Error Examples:

error: unknown constant 'Nat.lt_mul_of_one_lt_right'

error: type mismatch
  (Nat.mul_lt_mul_left h_k_pos).mpr hq_gt
has type
  k * 1 < k * q : Prop
but is expected to have type
  k * 1 * q > k * 1 : Prop

Request: Please provide the correct Lean 4.20 API and usage pattern to prove k * q > k given k > 1 and q > 1.

Additional Context: This is part of a larger project formalizing Vedic mathematical algorithms. We're using the proven Robin Arnez/Aaron Liu pattern for WellFounded termination. The mathematical reasoning is sound, we just need the correct Lean 4.20 API to express this basic multiplication inequality.

Thank you for any guidance you can provide!

[Robin Arnez]

notation "ℕ" => Nat

example (k q : ℕ) (hk_gt : 1 < k) (hq_gt : 1 < q) : k < k * q := by
  have : k * 1 < k * q := Nat.mul_lt_mul_of_pos_left hq_gt (Nat.lt_trans (by decide) hk_gt)
  simpa using this

[Philippe Duchon]

The very first non-comment line of your MWE fails - the file you are trying to import does not exist. It is hard to believe that this occurs in a genuine attempt at providing a MWE.

For your information, after importing Mathlib (probably overkill, but I leave it to you to get to minimal imports if that is a concern in your development), in your first example, trying apply? gives a suggestion that closes the goal.