proposition: Lemma ltBoolTrue : forall a b : nat, ltBool a b = true -> a < b.
proof: Proof. intros a b H; unfold ltBool in H. destruct (le_lt_dec b a); [discriminate | assumption]. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)