Library additions.BinaryStrat

Binary strategy, according to Bergeron, Brlek et al.

Let be a positive number. We associate to the half of .

From Coq Require Import Arith NArith Lia.
From additions Require Import Pow Compatibility More_on_positive.
From additions Require Export Strategies.

Open Scope positive_scope.

Definition half (p:positive) :=
  match p with xH ⇒ xH
          | xI q | xO q ⇒ q
  end.

Definition two (p:positive) := 2%positive.

#[ global ] Instance Binary_strat : Strategy half.

#[ global ] Instance Two_strat : Strategy two.