proposition: Lemma rem_lea_false_nseq : forall a b, rem_lea_false (nseq a false ++ b) = rem_lea_false b.
proof: Proof. by elim. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext