proposition: Theorem Zle_bool_spec : forall x y, Zle_bool_prop x y (Zle_bool x y).
proof: Proof. intros x y. generalize (Zle_is_le_bool x y). case Zle_bool ; intros (H1, H2) ; constructor. now apply H2. destruct (Zle_or_lt x y) as [H|H]. now specialize (H1 H). exact H. Qed.
imports: Coq(ZArith Lia Zquot)