instance instIsOrbifoldHAddNatProd {X Y : Type u} [DiffeologicalSpace X] [DiffeologicalSpace Y] {n m : ℕ} [hX : IsOrbifold n X] [hY : IsOrbifold m Y] : IsOrbifold (n + m) (X × Y)