proposition: Lemma srs_step_specI {u v a b n m} : map fst (u ++ [a] ++ [b] ++ v) = map fst ([sl] ++ repeat sb n ++ [sm] ++ repeat sb m ++ [sr]) -> srs_step_spec u v a b n m \/ (a.1 = sb.1 /\ b.1 = sb.1) \/ (a.1 = sb.1 /\ b.1 = sm.1) \/ (a.1 = sm.1 /\ b.1 = sb.1).
proof: Proof. move: u => [|? u]. { move: n => [|n]. - move=> [] *. left. by apply: srs_step0. - move=> [] *. left. apply: srs_step1; by [|lia]. } move=> [] _. rewrite -/(_ ++ _). elim /rev_ind: v. { rewrite app_nil_r ?map_app /=. rewrite ?app_assoc. move=> /app_inj_tail []. have [->|->] : m = 0 \/ m = (m - 1) + 1 by lia. - rewrite app_nil_r. move=> /app_inj_tail [] *. left. by apply: srs_step2. - rewrite repeat_app map_app ?app_assoc. move=> /app_inj_tail [] *. left. apply: srs_step3; by [|lia]. } move=> ? v _. rewrite ?map_app ?app_assoc. move=> /app_inj_tail [+] _. move=> + /ltac:(right). elim: u n. { move=> [|[|n]]. - move: m => [|m [] *]; [done | by tauto ]. - move=> [] *. by tauto. - move=> [] *. by tauto. } move=> ? u IH [|n]; last by move=> [_] /IH. move=> [_] {IH}. rewrite -?/(_ ++ _). elim: m u; first by case. move=> m IH [|? u]; last by move=> [_] /IH. move: m {IH} => [|m] []; [done | by tauto]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun