Logipedia-Jumb

nat.nat

nat.not_le_to_leb_false

nat.le_to_leb_true

nat.leb_true_to_le

nat.leb_elim

nat.sym_eq_leb_body_S

nat.eq_leb_body_S

nat.axiom_leb_body_S

nat.sym_eq_leb_body_O

nat.eq_leb_body_O

nat.axiom_leb_body_O

nat.sym_eq_leb

nat.eq_leb

nat.axiom_leb

nat.leb_body

nat.leb

nat.not_eq_to_eqb_false

nat.eq_to_eqb_true

nat.eqb_false_to_not_eq

nat.eqb_true_to_eq

nat.eqb_n_n

nat.eqb_elim

nat.sym_eq_eqb_body_S

nat.eq_eqb_body_S

nat.axiom_eqb_body_S

nat.sym_eq_eqb_body_O

nat.eq_eqb_body_O

nat.axiom_eqb_body_O

nat.sym_eq_eqb

nat.eq_eqb

nat.axiom_eqb

nat.eqb_body

nat.eqb

nat.minus_plus_plus_l

nat.minus_le_minus_minus_comm

nat.minus_minus_comm

nat.minus_minus

nat.minus_plus

nat.distributive_times_minus

nat.eq_minus_O

nat.not_eq_to_le_to_lt

nat.minus_le

nat.monotonic_le_minus_r

nat.le_plus_to_minus

nat.monotonic_le_minus_l

nat.plus_to_minus

nat.minus_to_plus

nat.plus_minus_m_m

nat.minus_plus_m_m

nat.plus_minus

nat.le_to_le_to_eq

nat.le_n_O_to_eq

nat.lt_to_not_eq

nat.le_n_O_elim

nat.lt_O_n_elim

nat.le_to_or_lt_eq

nat.decidable_lt

nat.decidable_le

nat.le_to_not_lt

nat.not_lt_to_le

nat.not_le_to_lt

nat.lt_to_not_le

nat.not_le_Sn_n

nat.not_le_S_S_to_not_le

nat.not_le_to_not_le_S_S

nat.not_le_Sn_O

nat.lt_plus_Sn_r

nat.lt_plus_to_minus_r

nat.lt_times

nat.lt_to_le_to_lt_times

nat.monotonic_lt_times_l

nat.monotonic_lt_times_r

nat.monotonic_lt_plus_l

nat.monotonic_lt_plus_r

nat.lt_O_S

nat.ltn_to_ltO

nat.lt_S_to_lt

nat.le_to_lt_to_lt

nat.lt_to_le_to_lt

nat.transitive_lt

nat.lt_to_le

nat.le_plus_to_minus_r

nat.le_plus_minus_m_m

nat.le_times

nat.monotonic_le_times_r

nat.le_plus_to_le_r

nat.le_plus_to_le

nat.le_plus_n_r

nat.le_plus_b

nat.le_plus_n

nat.le_plus

nat.monotonic_le_plus_l

nat.monotonic_le_plus_r

nat.le_S_S_to_le

nat.monotonic_pred

nat.le_pred_n

nat.transitive_le

nat.le_n_Sn

nat.le_O_n

nat.le_S_S

nat.lt_to_not_zero

nat.not_eq_O_S

nat.not_eq_S

nat.eq_minus_S_pred

nat.minus_n_n

nat.minus_n_O

nat.minus_O_n

nat.minus_S_S

nat.times_n_1

nat.times_times

nat.associative_times

nat.distributive_times_plus_r

nat.distributive_times_plus

nat.commutative_times

nat.times_n_Sm

nat.times_n_O

nat.times_O_n

nat.times_Sn_m

nat.injective_plus_r

nat.assoc_plus1

nat.associative_plus

nat.commutative_plus

nat.plus_n_Sm

nat.plus_n_O

nat.plus_O_n

nat.S_pred

nat.injective_S

nat.pred_Sn

nat.le_gen

nat.nat_elim2

nat.nat_case

nat.sym_eq_minus_body_S

nat.eq_minus_body_S

nat.axiom_minus_body_S

nat.sym_eq_minus_body_O

nat.eq_minus_body_O

nat.axiom_minus_body_O

nat.sym_eq_minus

nat.eq_minus

nat.axiom_minus

nat.minus_body

nat.minus

nat.sym_eq_times_body_S

nat.eq_times_body_S

nat.axiom_times_body_S

nat.sym_eq_times_body_O

nat.eq_times_body_O

nat.axiom_times_body_O

nat.sym_eq_times

nat.eq_times

nat.axiom_times

nat.times_body

nat.times

nat.sym_eq_plus_body_S

nat.eq_plus_body_S

nat.axiom_plus_body_S

nat.sym_eq_plus_body_O

nat.eq_plus_body_O

nat.axiom_plus_body_O

nat.sym_eq_plus

nat.eq_plus

nat.axiom_plus

nat.plus_body

nat.plus

nat.lt

nat.le_ind

nat.match_le_prop

nat.le_S

nat.le_n

nat.le

nat.not_zero

nat.pred

nat.nat_ind

nat.sym_eq_filter_nat_type_S

nat.eq_filter_nat_type_S

nat.axiom_filter_nat_type_S

nat.sym_eq_filter_nat_type_O

nat.eq_filter_nat_type_O

nat.axiom_filter_nat_type_O

nat.filter_nat_type

nat.sym_eq_match_nat_type_S

nat.eq_match_nat_type_S

nat.axiom_match_nat_type_S

nat.sym_eq_match_nat_type_O

nat.eq_match_nat_type_O

nat.axiom_match_nat_type_O

nat.match_nat_type

nat.match_nat_prop

nat.S

nat.O