fact: Fixpoint hb_strip inner outer := if inner is inn0 :: inn then if outer is out0 :: out then (head 0 out <= inn0 <= out0) && (hb_strip inn out) else false else if outer is out0 :: out then out == [::] else true.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition