proposition: Lemma test_bigop n : \big[(@alt _ _)/fail]_(i < n) (fail : M A) = fail.
proof: Proof. elim: n => [|n IH]; first by rewrite big_ord0. by rewrite big_ord_recr /= IH altmfail. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)