proposition: Lemma Zle_bool_addr : forall z x y, Zle_bool x y -> Zle_bool (x + z) (y + z).
proof: Proof. by move=> x y z h; rewrite Zle_bool_plus_mono // Zle_bool_refl. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith