proposition: Lemma low_fromNat n2 n1: forall m, low n2 (fromNat (n:=n2+n1) m) = fromNat (n:=n2) m.
proof: Proof. induction n2 => m //. by rewrite /= /joinlsb !beheadCons !theadCons/= IHn2. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec