proposition: Lemma H5loss_draw_ge ht i l : Hiv (i :: l) -> ht_valid ht -> draw <= f1 i -> edraw <= f2 eloss edraw ht i.
proof: Proof. move=> Hiv Hv. case: f1 (@H5loss_draw_draw ht i l Hiv Hv) (@H5loss_draw_win ht i l Hiv Hv) => //. by move=> _ /(_ (refl_equal _)) /(leq_trans _) H _; rewrite H. by move=> /(_ (refl_equal _)) /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)