proposition: Lemma makeOnes: forall n k (q: k + (n - k) = n), k <= n -> decB (shlBn #1 k) = tcast q (zero (n - k) ## ones k).
proof: Proof. move=> n k q le_k. apply toNat_inj. rewrite toNat_tcast toNat_decB toNatCat toNat_zero mul0n add0n. rewrite toNat_ones. case k_neqz: (shlBn #1 k == #0). + case ltn_k: (k < n). + move/eqP: k_neqz=>k_neqz. have: true = false=> //. have->: true = getBit (n := n) (shlBn #1 k) k by rewrite getBit_shlBn_true. have->: false = getBit (n := n) #0 k by rewrite getBit_zero. by rewrite k_neqz //. + have ->: k = n=> //. apply/eqP. by rewrite -[k == n]orbF -ltn_k -leq_eqVlt. + rewrite toNat_shlBn //. case k_eq_n: (k == n). + move/eqP: k_neqz=>k_neqz. exfalso. apply k_neqz. move/eqP: k_eq_n ->. by apply shlBn_overflow. + by rewrite ltn_neqAle k_eq_n le_k. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)