proposition: Lemma NoB_mul a b : N.mul (bin_of_nat a) (bin_of_nat b) = bin_of_nat (a * b).
proof: Proof. by rewrite - (nat_of_binK (_ * _)%num) nat_of_mul_bin !bin_of_natK. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)