fact: Fixpoint rem_lea_false s := match s with | [::] => [::] | true :: _ => s | _ :: t => rem_lea_false t end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext