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