proposition: Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'.
proof: Proof. intros x y; unfold leb. case_eq (Nat.leb x y); [| rewrite <- 2 Bool.not_true_iff_false]; rewrite <- Zle_is_le_bool; rewrite Nat.leb_le; rewrite Nat2Z.inj_le; auto. Qed.
imports: ZArith NPeano