changelog, a missing lemma, and test

doc/changelog/11-standard-library/18628-more_bitwise_in_Natural.rst

@@ -0,0 +1,50 @@
+- **Added:** to :g:`N` and :g:`Nat` lemmas
+  :g:`strong_induction_le`,
+  :g:`binary_induction`,
+  :g:`strong_induction_le`,
+  :g:`even_even`,
+  :g:`odd_even`,
+  :g:`odd_odd`,
+  :g:`even_odd`,
+  :g:`b2n_le_1`,
+  :g:`testbit_odd_succ'`,
+  :g:`testbit_even_succ'`,
+  :g:`testbit_div2`,
+  :g:`div2_0`,
+  :g:`div2_1`,
+  :g:`div2_le_mono`,
+  :g:`div2_even`,
+  :g:`div2_odd'`,
+  :g:`le_div2_diag_l`,
+  :g:`div2_le_upper_bound`,
+  :g:`div2_le_lower_bound`,
+  :g:`lt_div2_diag_l`,
+  :g:`le_div2`,
+  :g:`lt_div2`,
+  :g:`div2_decr`,
+  :g:`land_even_l`,
+  :g:`land_even_r`,
+  :g:`land_odd_l`,
+  :g:`land_odd_r`,
+  :g:`land_even_even`,
+  :g:`land_odd_even`,
+  :g:`land_even_odd`,
+  :g:`land_odd_odd`,
+  :g:`land_le_l`,
+  :g:`land_le_r`,
+  :g:`ldiff_even_l`,
+  :g:`ldiff_odd_l`,
+  :g:`ldiff_even_r`,
+  :g:`ldiff_odd_r`,
+  :g:`ldiff_even_even`,
+  :g:`ldiff_odd_even`,
+  :g:`ldiff_even_odd`,
+  :g:`ldiff_odd_odd`,
+  :g:`ldiff_le_l`,
+  :g:`shiftl_lower_bound`,
+  :g:`shiftr_upper_bound`,
+  :g:`ones_0`,
+  :g:`ones_succ`,
+  :g:`pow_lower_bound`
+  (`#18628 <https://github.com/coq/coq/pull/18628>`_,
+  by Pierre Rousselin).

test-suite/success/strong_and_binary_induction.v

@@ -53,3 +53,12 @@ Proof.
       apply N.add_le_mono; [| exact (N.le_refl _)].
       apply N.le_mul_l; discriminate.
 Qed.
+
+(* [binary_induction] is also available for [N] *)
+Lemma land_diag_binary_induction_test_N n : N.land n n = n.
+Proof.
+  induction n as [| n IH | n IH] using N.binary_induction.
+  - rewrite N.land_0_l; reflexivity.
+  - rewrite N.land_even_l, N.div2_even, IH; reflexivity.
+  - rewrite N.land_odd_l, N.odd_odd, N.div2_odd', IH; reflexivity.
+Qed.

theories/NArith/BinNat.v

@@ -897,6 +897,11 @@ Proof. now destruct a. Qed.
 
 Include NExtraPreProp <+ NExtraProp0.
 
+Lemma binary_induction (A : N -> Prop) :
+  A 0 -> (forall n, A n -> A (2 * n)) -> (forall n, A n -> A (2 * n + 1))
+  -> forall n, A n.
+Proof. apply Private_binary_induction; intros x y ->; reflexivity. Qed.
+
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
   layers. The use of [gt] and [ge] is hence not recommended. We provide