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