proposition: Lemma eval_rec3_correct n t (alpha beta : state) b : alpha < beta -> [/\ eval_rec n t b <= alpha -> eval_rec3 n t alpha beta b <= alpha, beta <= eval_rec n t b -> beta <= eval_rec3 n t alpha beta b & alpha <= eval_rec n t b <= beta -> eval_rec3 n t alpha beta b = eval_rec n t b].
proof: Proof. elim: n t alpha beta b => //= n IH t alpha beta b aLb. case: ieval => //; split. - rewrite -{1 3}(sflipK alpha) !sflip_le => H. apply: process_eval_rec3_correct_b (H). move=> i b1 /andP[H1 H2]; have [_ ->// _] := IH (flip t) _ _ i H1. by rewrite sflip_lt aLb le_win. - rewrite -{1 2}(sflipK beta) !sflip_le => H. apply: process_eval_rec3_correct_a H => //; last first. by rewrite sflip_lt. move=> b1 s1 /andP[H1 H2]. by have [/(_ H1)-> _ _] := (IH (flip t) (sflip beta) s1 b1 H2). rewrite -{1}(sflipK alpha) -{1}(sflipK beta) !sflip_le => /andP[H1 H2]. apply: process_eval_rec3_correct => //. - move=> i a1 /andP[H a1L]. by have [_ /(_ a1L)] := IH (flip t) _ a1 i H. - move=> i a1 b1 a1Lsb1 /andP[a1Le eLb1]. have [_ _ ->//]:= IH (flip t) a1 b1 i a1Lsb1. by rewrite a1Le. - by rewrite sflip_lt. - by rewrite le_win sflip_le ltnW. by rewrite H2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)