I've decided to cheat.
Fixpoint pred' (n1: Nat): Nat :=
match n1 with
| Empt => Empt
| Fill Zer n1 => Fill One (pred' n1)
| Fill One n1 => trim (Fill Zer n1)
end.
Definition pred (n1: Nat) (H1: Trim n1) (H2: comp n1 zer = Great): Nat :=
pred' n1.