fact: Definition nat_plus_perm102 : ∏ n0 n1 n2, n0 + n1 + n2 = n1 + n0 + n2 := λ n0 n1 n2, maponpaths (λ z, z + n2) (natpluscomm n0 n1).
imports: UniMath.Foundations.NaturalNumbers UniMath.Tactics.Utilities UniMath.Tactics.Abmonoids_Tactics