le_n: forall n : nat, n <= n
le_0_n: forall n : nat, 0 <= n
le_S: forall n m : nat, n <= m -> n <= S m
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
le_n_S: forall n m : nat, n <= m -> S n <= S m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
le_ind:
  forall (n : nat) (P : nat -> Prop),
  P n ->
  (forall m : nat, n <= m -> P m -> P (S m)) ->
  forall n0 : nat, n <= n0 -> P n0
le_sind:
  forall (n : nat) (P : nat -> SProp),
  P n ->
  (forall m : nat, n <= m -> P m -> P (S m)) ->
  forall n0 : nat, n <= n0 -> P n0
false: bool
true: bool
is_true: bool -> Prop
eq_true: bool -> Prop
negb: bool -> bool
xorb: bool -> bool -> bool
andb: bool -> bool -> bool
orb: bool -> bool -> bool
implb: bool -> bool -> bool
Nat.odd: nat -> bool
Nat.even: nat -> bool
BoolSpec: Prop -> Prop -> bool -> Prop
Number.number_beq: Number.number -> Number.number -> bool
Nat.eqb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
Number.uint_beq: Number.uint -> Number.uint -> bool
Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
Hexadecimal.hexadecimal_beq:
  Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
Number.int_beq: Number.int -> Number.int -> bool
Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
Nat.ltb: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Hexadecimal.int_beq: Hexadecimal.int -> Hexadecimal.int -> bool
Decimal.int_beq: Decimal.int -> Decimal.int -> bool
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
eq_true_rec_r:
  forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
eq_true_ind:
  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
eq_true_rect_r:
  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
eq_true_ind_r:
  forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true
eq_true_rect:
  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
bool_sind:
  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
eq_true_rec:
  forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
eq_true_sind:
  forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
Number.internal_uint_dec_bl1:
  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_lb:
  forall x y : Hexadecimal.hexadecimal,
  x = y -> Hexadecimal.hexadecimal_beq x y = true
Hexadecimal.internal_int_dec_lb0:
  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
Number.internal_number_dec_lb:
  forall x y : Number.number, x = y -> Number.number_beq x y = true
Decimal.internal_decimal_dec_lb:
  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
Hexadecimal.internal_int_dec_bl0:
  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
Number.internal_int_dec_lb1:
  forall x y : Number.int, x = y -> Number.int_beq x y = true
Number.internal_int_dec_bl1:
  forall x y : Number.int, Number.int_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_bl:
  forall x y : Hexadecimal.hexadecimal,
  Hexadecimal.hexadecimal_beq x y = true -> x = y
Number.internal_uint_dec_lb1:
  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
Decimal.internal_int_dec_bl:
  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
Decimal.internal_int_dec_lb:
  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
Number.internal_number_dec_bl:
  forall x y : Number.number, Number.number_beq x y = true -> x = y
Byte.of_bits:
  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
  Byte.byte
Byte.to_bits:
  Byte.byte ->
  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
Decimal.internal_decimal_dec_bl:
  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
Hexadecimal.internal_uint_dec_bl0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_bl:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_lb:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
Hexadecimal.internal_uint_dec_lb0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_true_intro:
  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
BoolSpec_ind:
  forall [P Q : Prop] (P0 : bool -> Prop),
  (P -> P0 true) ->
  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
BoolSpec_sind:
  forall [P Q : Prop] (P0 : bool -> SProp),
  (P -> P0 true) ->
  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
Byte.to_bits_of_bits:
  forall
    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
  Byte.to_bits (Byte.of_bits b) = b
bool_choice:
  forall [S : Set] [R1 R2 : S -> Prop],
  (forall x : S, {R1 x} + {R2 x}) ->
  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
mult_n_O: forall n : nat, 0 = n * 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
n_Sn: forall n : nat, n <> S n
pred_Sn: forall n : nat, n = Nat.pred (S n)
O_S: forall n : nat, 0 <> S n
f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
eq_S: forall x y : nat, x = y -> S x = S y
eq_add_S: forall n m : nat, S n = S m -> n = m
min_r: forall n m : nat, m <= n -> Nat.min n m = m
min_l: forall n m : nat, n <= m -> Nat.min n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
max_l: forall n m : nat, m <= n -> Nat.max n m = n
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
not_eq_S: forall n m : nat, n <> m -> S n <> S m
mult_n_Sm: forall n m : nat, n * m + n = n * S m
f_equal2_plus:
  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
f_equal2_nat:
  forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
  x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
Number.internal_number_dec_lb:
  forall x y : Number.number, x = y -> Number.number_beq x y = true
Number.internal_int_dec_lb1:
  forall x y : Number.int, x = y -> Number.int_beq x y = true
Number.internal_number_dec_bl:
  forall x y : Number.number, Number.number_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_lb:
  forall x y : Hexadecimal.hexadecimal,
  x = y -> Hexadecimal.hexadecimal_beq x y = true
Number.internal_int_dec_bl1:
  forall x y : Number.int, Number.int_beq x y = true -> x = y
Number.internal_uint_dec_lb1:
  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
Number.internal_uint_dec_bl1:
  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
Decimal.internal_decimal_dec_lb:
  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
Hexadecimal.internal_hexadecimal_dec_bl:
  forall x y : Hexadecimal.hexadecimal,
  Hexadecimal.hexadecimal_beq x y = true -> x = y
Hexadecimal.internal_int_dec_lb0:
  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
Hexadecimal.internal_int_dec_bl0:
  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
Decimal.internal_int_dec_lb:
  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
Decimal.internal_decimal_dec_bl:
  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
Decimal.internal_int_dec_bl:
  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
Decimal.internal_uint_dec_bl:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_lb:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
Hexadecimal.internal_uint_dec_lb0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
Hexadecimal.internal_uint_dec_bl0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_true_intro:
  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
bool_choice:
  forall [S : Set] [R1 R2 : S -> Prop],
  (forall x : S, {R1 x} + {R2 x}) ->
  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
Number.internal_number_dec_lb:
  forall x y : Number.number, x = y -> Number.number_beq x y = true
Number.internal_number_dec_bl:
  forall x y : Number.number, Number.number_beq x y = true -> x = y
Number.internal_int_dec_lb1:
  forall x y : Number.int, x = y -> Number.int_beq x y = true
Number.internal_int_dec_bl1:
  forall x y : Number.int, Number.int_beq x y = true -> x = y
Number.internal_uint_dec_lb1:
  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
Number.internal_uint_dec_bl1:
  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_lb:
  forall x y : Hexadecimal.hexadecimal,
  x = y -> Hexadecimal.hexadecimal_beq x y = true
Hexadecimal.internal_hexadecimal_dec_bl:
  forall x y : Hexadecimal.hexadecimal,
  Hexadecimal.hexadecimal_beq x y = true -> x = y
Hexadecimal.internal_int_dec_lb0:
  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
Hexadecimal.internal_int_dec_bl0:
  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
Decimal.internal_decimal_dec_lb:
  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
Decimal.internal_decimal_dec_bl:
  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
Decimal.internal_int_dec_lb:
  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
Decimal.internal_int_dec_bl:
  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
Hexadecimal.internal_uint_dec_bl0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_bl:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_lb:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
Hexadecimal.internal_uint_dec_lb0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
andb_true_intro:
  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h: n <> newdef n
h: n <> newdef n
h': newdef n <> n
The command has indeed failed with message:
[Focus] No such goal.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h': ~ P n
h: P n
h: P n
a: A
b: A
or_assoc: forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C
and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
eq_trans_assoc:
  forall [A : Type] [x y z t : A] (e : x = y) (e' : y = z) (e'' : z = t),
  eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
mult_n_Sm: forall n m : nat, n * m + n = n * S m
f_equal2_plus:
  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
nat_rect_plus:
  forall (n m : nat) {A : Type} (f : A -> A) (x : A),
  nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) =
  nat_rect (fun _ : nat => A)
    (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) 
    (fun _ : nat => f) n
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
Number.internal_number_dec_bl:
  forall x y : Number.number, Number.number_beq x y = true -> x = y
Number.internal_int_dec_bl1:
  forall x y : Number.int, Number.int_beq x y = true -> x = y
Number.internal_uint_dec_bl1:
  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
Hexadecimal.internal_hexadecimal_dec_bl:
  forall x y : Hexadecimal.hexadecimal,
  Hexadecimal.hexadecimal_beq x y = true -> x = y
Hexadecimal.internal_int_dec_bl0:
  forall x y : Hexadecimal.int, Hexadecimal.int_beq x y = true -> x = y
Decimal.internal_decimal_dec_bl:
  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
Decimal.internal_int_dec_bl:
  forall x y : Decimal.int, Decimal.int_beq x y = true -> x = y
Byte.of_bits:
  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
  Byte.byte
Byte.to_bits_of_bits:
  forall
    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
  Byte.to_bits (Byte.of_bits b) = b
Number.internal_number_dec_lb:
  forall x y : Number.number, x = y -> Number.number_beq x y = true
Number.internal_uint_dec_lb1:
  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
Number.internal_int_dec_lb1:
  forall x y : Number.int, x = y -> Number.int_beq x y = true
Decimal.internal_int_dec_lb:
  forall x y : Decimal.int, x = y -> Decimal.int_beq x y = true
Hexadecimal.internal_hexadecimal_dec_lb:
  forall x y : Hexadecimal.hexadecimal,
  x = y -> Hexadecimal.hexadecimal_beq x y = true
Hexadecimal.internal_int_dec_lb0:
  forall x y : Hexadecimal.int, x = y -> Hexadecimal.int_beq x y = true
Decimal.internal_decimal_dec_lb:
  forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
Byte.to_bits:
  Byte.byte ->
  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
Hexadecimal.internal_uint_dec_bl0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
Decimal.internal_uint_dec_lb:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, x0 = y -> Decimal.uint_beq x0 y = true) x
Decimal.internal_uint_dec_bl:
  forall x : Decimal.uint,
  (fun x0 : Decimal.uint =>
   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
Hexadecimal.internal_uint_dec_lb0:
  forall x : Hexadecimal.uint,
  (fun x0 : Hexadecimal.uint =>
   forall y : Hexadecimal.uint, x0 = y -> Hexadecimal.uint_beq x0 y = true) x
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
andb_true_intro:
  forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
Byte.to_bits_of_bits:
  forall
    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
  Byte.to_bits (Byte.of_bits b) = b
bool_choice:
  forall [S : Set] [R1 R2 : S -> Prop],
  (forall x : S, {R1 x} + {R2 x}) ->
  {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
Nat.two: nat
Nat.zero: nat
Nat.one: nat
Nat.succ: nat -> nat
Nat.log2: nat -> nat
Nat.sqrt: nat -> nat
Nat.square: nat -> nat
Nat.double: nat -> nat
Nat.pred: nat -> nat
Nat.ldiff: nat -> nat -> nat
Nat.tail_mul: nat -> nat -> nat
Nat.land: nat -> nat -> nat
Nat.div: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
Nat.lor: nat -> nat -> nat
Nat.lxor: nat -> nat -> nat
Nat.of_hex_uint: Hexadecimal.uint -> nat
Nat.of_uint: Decimal.uint -> nat
Nat.of_num_uint: Number.uint -> nat
length: forall [A : Type], list A -> nat
plus_n_O: forall n : nat, n = n + 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
mult_n_Sm: forall n m : nat, n * m + n = n * S m
Nat.land_comm: forall a b : nat, Nat.land a b = Nat.land b a
Nat.lor_comm: forall a b : nat, Nat.lor a b = Nat.lor b a
Nat.lxor_comm: forall a b : nat, Nat.lxor a b = Nat.lxor b a
Nat.lcm_comm: forall a b : nat, Nat.lcm a b = Nat.lcm b a
Nat.min_comm: forall n m : nat, Nat.min n m = Nat.min m n
Nat.gcd_comm: forall n m : nat, Nat.gcd n m = Nat.gcd m n
Bool.xorb_comm: forall b b' : bool, xorb b b' = xorb b' b
Nat.max_comm: forall n m : nat, Nat.max n m = Nat.max m n
Nat.mul_comm: forall n m : nat, n * m = m * n
Nat.add_comm: forall n m : nat, n + m = m + n
Bool.orb_comm: forall b1 b2 : bool, (b1 || b2)%bool = (b2 || b1)%bool
Bool.andb_comm: forall b1 b2 : bool, (b1 && b2)%bool = (b2 && b1)%bool
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
Nat.testbit_spec':
  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
Nat.pow_div_l:
  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
Nat.testbit_false:
  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
Nat.testbit_true:
  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.land_ones: forall a n : nat, Nat.land a (Nat.ones n) = a mod 2 ^ n
Nat.div_exact: forall a b : nat, b <> 0 -> a = b * (a / b) <-> a mod b = 0
Nat.testbit_spec':
  forall a n : nat, Nat.b2n (Nat.testbit a n) = (a / 2 ^ n) mod 2
Nat.pow_div_l:
  forall a b c : nat, b <> 0 -> a mod b = 0 -> (a / b) ^ c = a ^ c / b ^ c
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
Nat.testbit_false:
  forall a n : nat, Nat.testbit a n = false <-> (a / 2 ^ n) mod 2 = 0
Nat.testbit_true:
  forall a n : nat, Nat.testbit a n = true <-> (a / 2 ^ n) mod 2 = 1
iff_Symmetric: Symmetric iff
iff_Reflexive: Reflexive iff
impl_Reflexive: Reflexive Basics.impl
eq_Symmetric: forall {A : Type}, Symmetric eq
eq_Reflexive: forall {A : Type}, Reflexive eq
Equivalence_Symmetric:
  forall {A : Type} {R : Relation_Definitions.relation A},
  Equivalence R -> Symmetric R
Equivalence_Reflexive:
  forall {A : Type} {R : Relation_Definitions.relation A},
  Equivalence R -> Reflexive R
PER_Symmetric:
  forall {A : Type} {R : Relation_Definitions.relation A},
  PER R -> Symmetric R
PreOrder_Reflexive:
  forall {A : Type} {R : Relation_Definitions.relation A},
  PreOrder R -> Reflexive R
reflexive_eq_dom_reflexive:
  forall {A B : Type} {R' : Relation_Definitions.relation B},
  Reflexive R' -> Reflexive (eq ==> R')%signature
B.b: B.a
A.b: A.a
F.L: F.P 0
inr: forall {A B : Type}, B -> A + B
inl: forall {A B : Type}, A -> A + B
(use "About" for full details on the implicit arguments of inl and inr)
f: None = 0
partition_cons1:
  forall [A : Type] (f : A -> bool) (a : A) (l : list A) [l1 l2 : list A],
  partition f l = (l1, l2) ->
  f a = true -> partition f (a :: l) = (a :: l1, l2)