proposition: Lemma ltb_lt n m : (n <? m) = true <-> n < m.
proof: Proof. unfold ltb, lt. destruct compare; easy'. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass