proposition: Lemma eval_rec4_correct n t i : let f1 := eval_rec n t in let f2 := eval_rec4 n t in [/\ [/\ f1 i = loss -> f2 eloss edraw i = eloss, f1 i = draw -> edraw <= f2 eloss edraw i <= drawwin & f1 i = win -> drawwin <= f2 eloss edraw i], [/\ f1 i = win -> f2 edraw ewin i = ewin, f1 i = draw -> lossdraw <= f2 edraw ewin i <= draw & f1 i = loss -> f2 edraw ewin i <= lossdraw] & f2 eloss ewin i = f1 i].
proof: Proof. elim: n t i => /= [|n IH] t i; case: ieval => //; try by case. repeat split => //. - rewrite -(sflipK loss) => /sflip_inj H. rewrite -(esflipK eloss). apply: process_eval_rec4_draw_win_win H => // i1. by case: (IH (flip t) i1) => _ []. - rewrite -(sflipK draw) => /sflip_inj H. by apply: process_eval_rec4_draw_win_draw H _ => // i1; case: (IH (flip t) i1) => _ []. - rewrite -(sflipK win) => /sflip_inj H. by apply: process_eval_rec4_draw_win_loss H => // i1; case: (IH (flip t) i1) => _ []. - rewrite -(sflipK win) => /sflip_inj H. by apply: process_eval_rec4_loss_draw_loss H => i1; case: (IH (flip t) i1) => [] []. - rewrite -(sflipK draw) => /sflip_inj H. by apply: process_eval_rec4_loss_draw_draw H _ => // i1; case: (IH (flip t) i1) => [] []. - rewrite -(sflipK loss) => /sflip_inj H. by apply: process_eval_rec4_loss_draw_win H _ => // i1; case: (IH (flip t) i1) => [] []. apply: process_eval_rec4_loss_win => //. - by move=> i1; case: (IH (flip t) i1) => [] []. - by move=> i1; case: (IH (flip t) i1) => [] []. - by move=> i1; case: (IH (flip t) i1) => [] []. - by move=> i1; case: (IH (flip t) i1) => [] []. by rewrite -es2ns2esK; apply: le_ewin. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)