proposition: Lemma alpha_ltn n : alpha n < alpha n.+1.
proof: Proof. have bL1 := bL1. rewrite /alpha /=. set h := head _ _. have hP : 0 < h. rewrite /h. case: (alphal n) (@gt0_alphal n) => // c l /(_ c)-> //. by rewrite inE eqxx. set l1 := merge _ _ _. have hIl1 : head 1 l1 \in l1. have /= := alphal_neq_nil n.+1. by rewrite -/l1; case: l1 => //= c l; rewrite inE eqxx. suff hLi i : i \in l1 -> h < i. by apply/hLi/hIl1. rewrite mem_merge mem_cat. suff hLi1 : (i \in behead (alphal n)) -> h < i => [|H]. have [H1|H1] := boolP (_ \in alphal _); have [H2|H2] := boolP (_ \in alphal _); rewrite /= ?inE -/h //. - by case/orP=> [/eqP->|//]; rewrite ltn_Pmull. - by case/orP=> [/eqP->|//]; rewrite ltn_Pmull. by rewrite -orbA => /or3P[/eqP->|/eqP->|//]; rewrite ltn_Pmull. have hsSa : subseq [:: h; i] (alphal n). rewrite (_ : alphal n = h :: behead (alphal n)). rewrite (@cat_subseq _ [::h] _ [::h]) //. by rewrite sub1seq. by rewrite /h; case: (alphal n) (alphal_neq_nil n). rewrite ltn_neqAle. have /= := subseq_sorted leq_trans hsSa (sorted_alphal n). rewrite andbT => ->. have /= := subseq_uniq hsSa (uniq_alphal n). by rewrite inE. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra)