fact: Definition nat_plus_perm120 : ∏ n0 n1 n2, n0 + n1 + n2 = n2 + n0 + n1 := λ n0 n1 n2, pathscomp0 (natpluscomm (n0 + n1) n2) (pathsinv0 (natplusassoc n2 n0 n1)).
imports: UniMath.Foundations.NaturalNumbers UniMath.Tactics.Utilities UniMath.Tactics.Abmonoids_Tactics