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