fact: Fixpoint rowstepwest (r : Row) : Row := match r with | C x rs => match rs with | C y (C z rs') => match move (tri z y x) with | CAN (tri z' y' x') => C x' (C y' (C z' rs')) | CANT => C x (rowstepwest rs) end | _ => r end | Nil => Nil end.