Show existence of stucture

Stream: new members

[Gregor Kikelj]

Beginner here, I want to show that some object exists, but need to make a lemma first. Here is what I tried, but not sure how to fix it.

structure dpair (a b:nat):=
(alb: a < b)


def dpairmk (a b:nat) (c: a < b): dpair a b:=
  {alb:=c}

lemma exists_dpair : ∃ a b c, dpairmk a b c :=
begin
  sorry,
end

[Gregor Kikelj]

Here's the error message, so I guess the approach isn't very good :)

type mismatch at application
  ∃ (c : a < b), dpairmk a b c
term
  λ (c : a < b), dpairmk a b c
has type
  a < b → dpair a b
but is expected to have type
  a < b → Prop

[Yaël Dillies]

What should that mean? dpairmk a b c is a definition. What does it mean for a definition to exist?

[Gregor Kikelj]

I was thinking that dpairmk is something that gives me a dpair from a b and proof that (a<b)

[Yaël Dillies]

Yes, so what you want is

lemma exists_dpair : ∃ a b, nonempty (dpair a b) := sorry

maybe?

[Gregor Kikelj]

Thanks a lot, exactly what I need :)