proposition: Theorem ltb_lt p q : (p <? q) = true <-> p < q.
proof: Proof. unfold ltb, lt. destruct compare; easy'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef