proposition: Lemma ltBoolFalse : forall a b : nat, ltBool a b = false -> ~ a < b.
proof: Proof. intros a b H; unfold ltBool in H. destruct (le_lt_dec b a). - unfold not ; intros; lia. - discriminate. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)