proposition: Lemma H4draw_win_ge i : draw <= f1 i -> lossdraw <= f2 edraw ewin i.
proof: Proof. case: f1 (@H4draw_win_draw i) (@H4draw_win_win i) => //. by move=> _ /(_ (refl_equal _))->. by move=> /(_ (refl_equal _)) /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)