proposition: Fact ex_dropeq s1 s2 : exists n, drop n s1 == drop n s2.
proof: Proof. exists (maxn (size s1) (size s2)). by rewrite !drop_oversize ?leq_maxr ?leq_maxl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition