proposition: Theorem negb_Zlt_bool : forall x y : Z, negb (Zlt_bool x y) = Zle_bool y x.
proof: Proof. intros x y. case Zlt_bool_spec ; intros H. now rewrite Zle_bool_false. now rewrite Zle_bool_true. Qed.
imports: Coq(ZArith Lia Zquot)