contrapose reverting `Prop` as `forall`

Stream: new members

[Vivek Rajesh Joshi]

Why is contrapose adding h as a \forall to the goal instead of switching the goal and h?

import Mathlib.Data.Matrix.Notation
variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

abbrev colListofMat := List.map List.ofFn (List.ofFn M.transpose)

def list_allZero (l : List Rat) : Bool := l.all (fun x => (x==0))

def findNonzCol : ℕ := (colListofMat M).findIdx (fun col => ¬ list_allZero col)

lemma findNonzCol_get_HasNonz (h : findNonzCol M < (colListofMat M).length) :
  ∃ x ∈ (colListofMat M).get ⟨findNonzCol M,h⟩, x≠0 := by
  contrapose h

[Vincent Beffara]

h occurs in the goal

[Vivek Rajesh Joshi]

I see, thanks.