proposition: Lemma gt0_alphal n i : i \in alphal n -> 0 < i.
proof: Proof. have bL1 := bL1. elim: n i => /= [i|n]. by rewrite !inE => /or3P[] /eqP-> //; rewrite ltnW // (ltn_trans aL1). case: (alphal n) => [/= _ i|/= a1 l IH i]; rewrite !inE. by case/orP=> /eqP->; rewrite muln1 ltnW. have H1 : 0 < a1 by apply: IH; rewrite inE eqxx. have IH1 i1 : i1 \in l -> 0 < i1. by move=> U; apply: IH; rewrite inE orbC U. rewrite mem_merge. (do 2 case: (_ || _)); rewrite //= ?inE; first by apply: IH1. - by case/orP=> [/eqP->|/IH1//]; rewrite muln_gt0 ltnW. - by case/orP=> [/eqP->|/IH1//]; rewrite muln_gt0 ltnW. by case/or3P=> [/eqP->|/eqP->|/IH1//]; rewrite muln_gt0 ltnW. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)