Coq で、Coq.Arith.Compare_dec と Coq.Numbers.Natural.Peano.NPeano の両方に leb が定義されているのはなんでかな。
実装は違うが、以下のように等価性を証明できるので、意味が違うということではないようだ。
Require Import Compare_dec.
Require Import NPeano.
Goal forall (n m:nat), Compare_dec.leb n m = NPeano.leb n m.
Proof.
intros n.
induction n.
intros m.
simpl.
reflexivity.
intros m.
simpl.
destruct m.
reflexivity.
apply (IHn m).
Qed.[latest]