proposition: Lemma blt_ok : forall f g, blt f g = true <-> lt f g.
proof: Proof. intros f g. unfold blt, lt. apply bgt_nat_ok. Qed.
imports: CoLoR(EqUtil ListUtil LogicUtil) Coq(DecidableType) CoLoR(NatUtil BoolUtil) Coq(OrderedType)