proposition: Lemma bits_cat p a : bits p a = bits p [::] ++ a.
proof: Proof. elim: p a => [ p Ih | p Ih | ] /= a; rewrite ?(Ih (_ :: a)) ?(Ih (_ :: nil)) -?catA //. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)