proposition: Lemma H5draw_win_table ht i l : Hiv (i :: l) -> ht_valid ht -> ht_valid (f2 edraw ewin ht i).
proof: Proof. by move/Hiv_hd=> [] _ [H _ _ _] _; apply: H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)