proposition: Lemma mod_pow2_bits_high : forall a n m, n<=m -> (a mod 2^n).[m] = false.
proof: Proof. intros a n m H. destruct (eq_0_gt_0_cases (a mod 2^n)) as [EQ|LT]. - now rewrite EQ, bits_0. - apply bits_above_log2. apply lt_le_trans with n; trivial. apply log2_lt_pow2; trivial. apply mod_upper_bound; order_nz. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog