proposition: Remark size_merge_sort_push s1 : let graded ss := forall i, size (nth [::] ss i) \in pred2 0 (2 ^ (i + 1)) in size s1 = 2 -> {homo merge_sort_push s1 : ss / graded ss}.
proof: Proof. set n := {2}1; rewrite -[RHS]/(2 ^ n) => graded sz_s1 ss. elim: ss => [|s2 ss IHss] in (n) graded s1 sz_s1 * => sz_ss i //=. by case: i => [|[]] //; rewrite sz_s1 inE eqxx orbT. case: s2 i => [|x s2] [|i] //= in sz_ss *; first by rewrite sz_s1 inE eqxx orbT. exact: (sz_ss i.+1). rewrite addSnnS; apply: IHss i => [|i]; last by rewrite -addSnnS (sz_ss i.+1). by rewrite size_merge size_cat sz_s1 (eqP (sz_ss 0)) addnn expnS mul2n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)