sort.idr

module ListProof

import Prelude.List
import Prelude.Nat
import Prelude.Bool

%access public export

ifelse : (b : Bool) -> (t : a) -> (e : a) -> a
ifelse False t e = e
ifelse True t e = t

placeSorted : (n : Nat) -> (l : List Nat) -> List Nat
placeSorted n [] = [n]
placeSorted n (x :: xs) =
  ifelse (n <= x)  (n :: x :: xs) (x :: (placeSorted n xs))

bubbleSortNat : (l : List Nat) -> List Nat
bubbleSortNat [] = []
bubbleSortNat (x :: xs) =
  let nl = bubbleSortNat xs in
      placeSorted x nl

testSort : bubbleSortNat [3, 2, 4, 1] = [1, 2, 3, 4]
testSort = Refl

msorted : (l : List Nat) -> Bool
msorted [] = True
msorted (x :: []) = True
msorted (x :: (y :: xs)) = ifelse (x <= y) (msorted (y :: xs)) False

testSorted : msorted [3, 2, 4, 1] = False
testSorted = Refl

lemMsorted : (x : Nat) -> (xs : List Nat) -> msorted (x :: xs) = True -> msorted xs = True
lemMsorted x [] prf = Refl
lemMsorted x (y :: ys) prf with (x <= y) proof p
  lemMsorted x (y :: ys) prf | True = prf
  lemMsorted x (y :: ys) prf | False = absurd prf


placeSortedProof : (x : Nat) -> (xs : List Nat) -> msorted xs = True -> msorted (placeSorted x xs) = True
placeSortedProof x [] prf = Refl
placeSortedProof x (y :: xs) prf with (x <= y) proof p
  placeSortedProof x (y :: xs) prf | True = rewrite sym p in prf
  placeSortedProof x (y :: xs) prf | False = ?placeSortedProof_rhs

You need to mirror the structure of msorted:

placeSortedProof : (x : Nat) -> (xs : List Nat) -> msorted xs = True -> msorted (placeSorted x xs) = True
placeSortedProof x [] prf = Refl
placeSortedProof x [y] prf with (x <= y) proof p 
  placeSortedProof x [y] prf | True = rewrite sym p in Refl
  placeSortedProof x [y] prf | False = ?wat
placeSortedProof x (y :: y' :: ys) prf with (x <= y) proof p
  placeSortedProof x (y :: y' :: ys) prf | True = rewrite sym p in prf
  placeSortedProof x (y :: y' :: ys) prf | False with (x <= y') proof p'
    placeSortedProof x (y :: y' :: ys) prf | False | True = rewrite sym p' in ?wat2
    placeSortedProof x (y :: y' :: ys) prf | False | False = let tt = placeSortedProof x ys ?prf in ?wat3

To fill wat and wat2 you also need functions to rotate inequalities ala x<=y = False -> y<x = True.
For wat3 you'll also need a lemma that y < x = True -> msorted (placeSorted x xs) = True -> msorted (y :: placeSorted x xs) = True
(Also you might as well switch to So)