intro i j
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
⊢ propsAB fun i j => a (p i) (p j)
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0