regular.lean

lemma sizeof_drop_lt_sizeof {α : Type} {n : ℕ} {xs : list α} :
    list.sizeof (drop n xs) < 1 + list.sizeof xs :=
begin
    induction n generalizing xs,
    case nat.zero {
        apply nat.lt_add_of_pos_left,
        constructor,
    },
    case nat.succ n' ih_n {
        cases xs,
        case nil {
            unfold list.sizeof,
            constructor,
        },
        case cons x' xs' {
            unfold drop,
            apply lt_trans ih_n,
            unfold list.sizeof,
            apply add_lt_add_left,
            apply lt_add_of_pos_left,
            constructor,
        },
    },
end

lemma sizeof_drop_lt_sizeof' {α : Type} : ∀ {n : ℕ} {xs : list α},
    list.sizeof (drop n xs) < 1 + list.sizeof xs
| 0     _       := nat.lt_add_of_pos_left (by constructor)
| (n+1) []      := by { rw list.sizeof, constructor }
| (n+1) (x::xs) := by {
    unfold drop,
    apply lt_trans sizeof_drop_lt_sizeof',
    unfold list.sizeof,
    apply add_lt_add_left,
    apply lt_add_of_pos_left,
    constructor,
}