Library fl.aut.misc

(*
    Authors: Thierry Coquand, Vincent Siles
*)

Set Implicit Arguments.

Module Misc.

  Section Language.

    Variable char: finType.
    Definition word := seq char.
    Definition language := pred word.

  End Language.

  Lemma ltn_trans_tight m n p : m < n → n < p → m < p.-1.

  Lemma ltn_trans_tight' m n p : m < n → n < p.-1 → m < p.-1.

  Lemma size_induction {X : Type} (f : X → nat) (p: X →Prop) :
    ( ∀ x, ( ∀ y, f y < f x → p y) → p x) → ∀ x, p x.

End Misc.