proposition: Lemma rem_lea_false_pad_seqL : forall a l, (size l < a)%nat -> rem_lea_false (pad_seqL false (true :: l) a) = true :: l.
proof: Proof. case=> [//| a l H]. by rewrite /pad_seqL /= H subSS rem_lea_false_nseq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext