proposition: Lemma H5draw_win_le ht i l : Hiv (i :: l) -> ht_valid ht -> f1 i <= draw -> f2 edraw ewin ht i <= edraw.
proof: Proof. move=> HHiv Hv. case: f1 (@H5draw_win_loss ht i l HHiv Hv) (@H5draw_win_draw ht i l HHiv Hv) => //. by move=> /(_ (refl_equal _)) /leq_trans->. by move=> _ /(_ (refl_equal _)) /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)