have h_gbs := groupBySubtractive_spec7 t c hc
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
⊢ nrows (groupBySubtractive t c) ≤ nrows t
η : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq η
inst✝ : DecidableEq τ
schema : Schema
t : Table schema
c : η
hc : Schema.HasCol (c, τ) schema
h_gbs : nrows (groupBySubtractive t c) = List.length (List.unique (getColumn2 t c))
⊢ nrows (groupBySubtractive t c) ≤ nrows t