gistfile1.txt

import data.list.basic

lemma list.nil_le {α : Type*} [linear_order α] (L : list α) : [] ≤ L := 
begin
  cases L,
  { left, refl, },
  { right, constructor, },
end

lemma list.nil_lt {α : Type*} [linear_order α] (a : α) (L : list α) : [] < a :: L := 
begin
  constructor,
end

lemma list.cons_le_iff {α : Type*} [linear_order α] (a a' : α) (L L' : list α) : 
  a :: L ≤ a' :: L' ↔ (a < a') ∨ (a = a' ∧ L ≤ L') :=
begin
  fsplit,
  { intro h, 
    cases h, 
    { injections with ha hL,
      right, 
      split,
      assumption, 
      left,
      assumption, }, 
    { cases h, 
      { right, 
        split,
        refl, 
        right, 
        assumption, },
      { left, assumption, }}},
  { intro h, 
    cases h,
    { right, constructor, assumption, },
    { rcases h with ⟨rfl, ⟨rfl|h⟩⟩,
      { left, refl, },
      { right, constructor, assumption, }} },
end