The product of two AddMonoidWithOnes.

@[instance_reducible]

instance Prod.instAddMonoidWithOne {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] : AddMonoidWithOne (α × β)

@[simp]

theorem Prod.fst_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) : (↑n).1 = ↑n

@[simp]

theorem Prod.fst_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).1 = OfNat.ofNat n

@[simp]

theorem Prod.snd_natCast {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) : (↑n).2 = ↑n

@[simp]

theorem Prod.snd_ofNat {α : Type u_1} {β : Type u_2} [AddMonoidWithOne α] [AddMonoidWithOne β] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).2 = OfNat.ofNat n