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