add new proof

src/Data/Nat.hs

@@ -174,6 +174,11 @@ plus_commut n  SZ    = plus_right_id n
 plus_commut n  (SS m) =
   sym (succ_right n m) ∾ cong SS (plus_commut n m) ∾ succ_left m n
 
+-- | Left identity of multiplication
+cross_left_id ∷ Sℕ n →  (S Z) :× n :≡ n
+cross_left_id SZ     = Refl
+cross_left_id (SS n) = cong SS (cross_left_id n)
+
 -- | Minimum of itself
 min_self ∷ Sℕ n → Min n n :≡ n
 min_self SZ     = Refl