Positive partial transpose of separable state

import Separable
import Partial_transpose


/--
A separable state stays positive
after a partial transpose acts
on either system. 
-/
lemma pos_part_transpose_of_separable_state [quantum_state ρ]:
separable ρ → PPT ρ :=
begin
  -- rw separable as sum of tensor products,
  -- have partial transpose is a linear channel,
  -- have partial tranpose does not change the trace,
  -- have the state after partial transpose is positive.
  sorry,
end

Works for more than two systems.