proposition: Theorem Zlt_bool_false : forall x y : Z, (y <= x)%Z -> Zlt_bool x y = false.
proof: Proof. intros x y Hxy. generalize (Zlt_cases x y). case Zlt_bool ; intros H. elim (Z.lt_irrefl x). now apply Z.lt_le_trans with y. apply refl_equal. Qed.
imports: Coq(ZArith Lia Zquot)