proposition: Lemma enumE : enum X = [:: a; b; c].
proof: Proof. apply (@eq_from_nth _ a); first by rewrite -cardE X3. case=> [_|]; first by rewrite [X in _ = X]/= {2}/a (enum_val_nth a). case=> [_|]; first by rewrite [X in _ = X]/= {1}/b (enum_val_nth a). case=> [_|]; first by rewrite [X in _ = X]/= {1}/c (enum_val_nth a). move=> n; rewrite -cardE X3; by case: n. Qed.
imports: Reals Lra mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra reals Rstruct) infotheo(ssrR realType_ext Reals_ext proba) monae_lib hierarchy monad_lib fail_lib proba_lib