proposition: Lemma Useless_steps_shorter (r:route) : Useless_steps_in r -> {r' : route | r =r= r' /\ (length r' < length r)%nat}.
proof: Proof. intro H;destruct H as [r0 r1 r2 d d1 H1 H2]. exists (r0 ++ r1 ++ r2). split. - subst r; replace (r0 ++ (d :: r1) ++ d1 :: r2) with (r0 ++ ((d::nil) ++ r1) ++ ((d1::nil)++r2)) by (simpl;auto). apply app_route_Proper;[reflexivity|]. rewrite app_assoc. apply app_route_Proper;[|reflexivity]. transitivity ((d1::nil)++(d::r1)). rewrite app_comm; reflexivity. simpl;rewrite opposite_cons;[reflexivity|trivial]. - subst r; repeat (simpl;repeat rewrite app_length); lia. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia