le_S: forall n m : nat, n <= m -> n <= S m
le_n: forall n : nat, n <= n
false: bool
true: bool
xorb: bool -> bool -> bool
orb: bool -> bool -> bool
negb: bool -> bool
implb: bool -> bool -> bool
andb: bool -> bool -> bool
pred_Sn: forall n : nat, n = pred (S n)
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_n_O: forall n : nat, n = n + 0
plus_Sn_m: forall n m : nat, S n + m = S (n + m)
plus_O_n: forall n : nat, 0 + n = n
mult_n_Sm: forall n m : nat, n * m + n = n * S m
mult_n_O: forall n : nat, 0 = n * 0
eq_add_S: forall n m : nat, S n = S m -> n = m
eq_S: forall x y : nat, x = y -> S x = S y