fact: Definition nat_mult_perm210 : ∏ n0 n1 n2, n0 * n1 * n2 = n2 * n1 * n0 := λ n0 n1 n2, pathscomp0 (nat_mult_perm102 n0 n1 n2) (nat_mult_perm120 n1 n0 n2).
imports: UniMath.Foundations.NaturalNumbers UniMath.Tactics.Utilities UniMath.Tactics.Abmonoids_Tactics