proposition: Theorem negb_Zle_bool : forall x y : Z, negb (Zle_bool x y) = Zlt_bool y x.
proof: Proof. intros x y. case Zle_bool_spec ; intros H. now rewrite Zlt_bool_false. now rewrite Zlt_bool_true. Qed.
imports: Coq(ZArith Lia Zquot)