proposition: Lemma nat_of_add_bin b1 b2 : (b1 + b2)%num = b1 + b2 :> nat.
proof: Proof. by case: b1 b2 => [|p] [|q]; rewrite ?addn0 //= nat_of_add_pos. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring