Logipedia
Modules
About
FAQ
Search
Search
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