Using An Existing Theorem: Simple Example

Stream: new members

[Dev-Indra]

Based on the Natural Number Game, we have this theorem: lean le_iff_exists_add. As a simple exercise I wish to prove this:

theorem ge_iff_exists_add (a b: ℕ): a ≥ b ↔ ∃ (c: ℕ), a = b + c :=
begin

end

I tried using the le_iff_exists_add theorem to prove this but to no avail. Does anyone know how to use this existing theorem to prove my elementary theorem (or better yet so that I can practice, does anyone know the the proof for le_iff_exists_add so that I can adapt it to prove mine?)

[Dev-Indra]

I just realized there was a typo in the theorem above. Here is the theorem (same question as above though):

theorem g_iff_exists_add (a b: ℕ): a > b ↔ ∃ (c: ℕ) (c ≥ 1), a = b + c :=
begin

end

[Anne Baanen]

Here's the proof for le_iff_exists_add on natural numbers.

[Anne Baanen]

To go from a = b + c, it does induction on c, and to go from a ≤ b, it does induction on the proof that a ≤ b

[Dev-Indra]

@Anne Baanen Thanks for the code. I will look through it.
So for the latter case, what would be statement be to start the induction, something like induction [what here?]...?

[Dev-Indra]

In the NNG I only saw uses of induction a with v hv but not on a proof.

[Anne Baanen]

If you have h : a > b, you can write induction h, for example:

theorem gt_iff_exists_add (a b : ℕ) : a > b ↔ ∃ (c : ℕ) (c ≥ 1), a = b + c :=
begin
  apply iff.intro,
  { intro h, -- h : a > b
    induction h,
    { sorry },
    sorry },
  intro h,
  sorry
end

[Anne Baanen]

Inductive propositions is something that you don't encounter a lot in pen-and-paper mathematics, but the idea is similar to inductive data types like the natural numbers. Like the natural numbers are the smallest type nat with 0 : nat and succ : nat -> nat and no other relations, nat.le is the smallest type such that refl : a ≤ a and step : ∀ b, a ≤ b -> a ≤ succ b

[Anne Baanen]

You might have encountered definitions of the form "S is the smallest subset of α such that 0 ∈ S and if a, b ∈ S then a + b ∈ S". With such sets, you can also do a kind of induction: to prove some proposition P x, it suffices to show P 0 and if P a and P b, then P (a + b). In type theory, you can use an inductive type to define x ∈ S.

[Dev-Indra]

Thanks I will give this a try