proposition: Lemma NoB_ler a b: N.le (bin_of_nat a) (bin_of_nat b) -> a <= b.
proof: Proof. move => h; case: (leqP a b) => // lba; case /N.nlt_ge:h. by rewrite - (subnKC lba) addSnnS - NoB_add; apply:N.lt_add_pos_r. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)