proposition: Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'.
proof: Proof. intros x y; unfold ltb. case_eq (Nat.ltb x y); [| rewrite <- 2 Bool.not_true_iff_false]; rewrite <- Zlt_is_lt_bool; rewrite Nat.ltb_lt; rewrite Nat2Z.inj_lt; auto. Qed.
imports: ZArith NPeano