Lemma testlemma9 : hzlth 0 ( nattohz 9 ). Proof. apply ( istranshzlth _ ( nattohz 3 ) ). - apply testlemma3. - apply ( istranshzlth _ ( nattohz 6 ) ). + apply testlemma3. + apply testlemma3. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.