Coqにも型クラスがあるらしいです。

Class Ord a :=
  {
    le : a -> a -> bool
  }.

これでleというメソッドを持つ型クラスOrdを定義できます。

インスタンス定義は以下のように行います。

Fixpoint le_nat (n m : nat) : bool :=
  match n, m with
    | O, O => true
    | O, S _ => true
    | S _, O => false
    | S n', S m' => le_nat n' m'
  end.

Instance nat_ord : Ord nat :=
  {
    le := le_nat
  }.

複数のインスタンスを定義することもできます。

Instance nat_rev_ord : Ord nat :=
  {
    le := fun x y => le_nat y x
  }.

どのインスタンスを選択するかは、

@le nat nat_rev_ord

のように明示的に与えてやればOKです。

Coqにはそもそも暗黙引数があるので、型クラスがあるからと言って無い場合に比べてめちゃくちゃ便利になるかと言われるとそういうことも無さそうです。暗黙引数でレコード型を渡すのと書き方的にもそんなに変わりません。