Skip to content

Instantly share code, notes, and snippets.

@banbh

banbh/lt_aux_two.lean

Created December 8, 2019 20:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save banbh/2ef6a84caac87fd2d5e656b1884203cc to your computer and use it in GitHub Desktop.
Save banbh/2ef6a84caac87fd2d5e656b1884203cc to your computer and use it in GitHub Desktop.
Download ZIP
Proving lt_aux_two using transitivity
Raw
lt_aux_two.lean
lemma lt_aux_two (a b : mynat) : succ a ≤ b → a ≤ b ∧ ¬ (b ≤ a) :=
begin
intro h,
split,
exact le_trans _ _ _ (le_succ_self a) h,
intro h2,
exact not_succ_le_self _ (le_trans _ _ _ h h2),
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment