proposition: Lemma H4loss_draw_le i : f1 i <= draw -> f2 eloss edraw i <= drawwin.
proof: Proof. case: f1 (@H4loss_draw_loss i) (@H4loss_draw_draw i) => //. by move=> /(_ (refl_equal _))->. by move=> _ /(_ (refl_equal _)) /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)