proposition: Fact bound_step m n i j : (i < 2 ^ m -> j < 2 ^ n -> j + i * 2 ^ n.+1 + 2 ^ n < 2 ^ (m + n).+1)%N.
proof: Proof. move=> Hi Hj. rewrite addnAC. apply: leq_trans (_ : 2 ^ n + 2 ^ n + i *2 ^ n.+1 <= _ )%N. by rewrite -!addnA ltn_add2r. by rewrite addnn -mul2n -expnS -mulSn -addnS expnD leq_mul2r expn_eq0 /=. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn