proposition: Lemma pow2_le: forall n m, (n <= m)%nat -> (pow2 n <= pow2 m)%nat.
proof: Proof. intros. assert (exists s, n + s = m) by (exists (m - n); lia). destruct H0; subst. rewrite pow2_add_mul. pose proof (pow2_zero x). replace (pow2 n) with (pow2 n * 1) at 1 by lia. apply mul_le_mono_l. lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega