fact: Definition ℤBiRecursionData (P:ℤ->Type) (IH :∏ i, P(i) -> P(1+i)) := fun f:∏ i, P i => ∏ i, f(1+i)=IH i (f i).
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.MoreEquivalences UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.GroupAction UniMath.NumberSystems.Integers