proposition: Theorem Zle_bool_opp_l : forall x y, Zle_bool (Z.opp x) y = Zle_bool (Z.opp y) x.
proof: Proof. intros x y. case Zle_bool_spec ; intros Hxy ; case Zle_bool_spec ; intros Hyx ; try easy ; lia. Qed.
imports: Coq(ZArith Lia Zquot)