axiom
- sttfa:nat/match_nat_prop.axm
- sttfa:nat/axiom_match_nat_type_O.axm
- sttfa:nat/axiom_match_nat_type_S.axm
- sttfa:nat/axiom_filter_nat_type_O.axm
- sttfa:nat/axiom_filter_nat_type_S.axm
- sttfa:nat/nat_ind.axm
- sttfa:nat/le_n.axm
- sttfa:nat/le_S.axm
- sttfa:nat/match_le_prop.axm
- sttfa:nat/le_ind.axm
- sttfa:nat/axiom_plus.axm
- sttfa:nat/axiom_plus_body_O.axm
- sttfa:nat/axiom_plus_body_S.axm
- sttfa:nat/axiom_times.axm
- sttfa:nat/axiom_times_body_O.axm
- sttfa:nat/axiom_times_body_S.axm
- sttfa:nat/axiom_minus.axm
- sttfa:nat/axiom_minus_body_O.axm
- sttfa:nat/axiom_minus_body_S.axm
- sttfa:nat/axiom_eqb.axm
- sttfa:nat/axiom_eqb_body_O.axm
- sttfa:nat/axiom_eqb_body_S.axm
- sttfa:nat/axiom_leb.axm
- sttfa:nat/axiom_leb_body_O.axm
- sttfa:nat/axiom_leb_body_S.axm
constant
- sttfa:nat/nat.cst
- sttfa:nat/O.cst
- sttfa:nat/S.cst
- sttfa:nat/match_nat_type.cst
- sttfa:nat/filter_nat_type.cst
- sttfa:nat/le.cst
- sttfa:nat/plus.cst
- sttfa:nat/plus_body.cst
- sttfa:nat/times.cst
- sttfa:nat/times_body.cst
- sttfa:nat/minus.cst
- sttfa:nat/minus_body.cst
- sttfa:nat/eqb.cst
- sttfa:nat/eqb_body.cst
- sttfa:nat/leb.cst
- sttfa:nat/leb_body.cst
definition
theorem
- sttfa:nat/eq_match_nat_type_O.thm
- sttfa:nat/sym_eq_match_nat_type_O.thm
- sttfa:nat/eq_match_nat_type_S.thm
- sttfa:nat/sym_eq_match_nat_type_S.thm
- sttfa:nat/eq_filter_nat_type_O.thm
- sttfa:nat/sym_eq_filter_nat_type_O.thm
- sttfa:nat/eq_filter_nat_type_S.thm
- sttfa:nat/sym_eq_filter_nat_type_S.thm
- sttfa:nat/eq_plus.thm
- sttfa:nat/sym_eq_plus.thm
- sttfa:nat/eq_plus_body_O.thm
- sttfa:nat/sym_eq_plus_body_O.thm
- sttfa:nat/eq_plus_body_S.thm
- sttfa:nat/sym_eq_plus_body_S.thm
- sttfa:nat/eq_times.thm
- sttfa:nat/sym_eq_times.thm
- sttfa:nat/eq_times_body_O.thm
- sttfa:nat/sym_eq_times_body_O.thm
- sttfa:nat/eq_times_body_S.thm
- sttfa:nat/sym_eq_times_body_S.thm
- sttfa:nat/eq_minus.thm
- sttfa:nat/sym_eq_minus.thm
- sttfa:nat/eq_minus_body_O.thm
- sttfa:nat/sym_eq_minus_body_O.thm
- sttfa:nat/eq_minus_body_S.thm
- sttfa:nat/sym_eq_minus_body_S.thm
- sttfa:nat/nat_case.thm
- sttfa:nat/nat_elim2.thm
- sttfa:nat/le_gen.thm
- sttfa:nat/pred_Sn.thm
- sttfa:nat/injective_S.thm
- sttfa:nat/S_pred.thm
- sttfa:nat/plus_O_n.thm
- sttfa:nat/plus_n_O.thm
- sttfa:nat/plus_n_Sm.thm
- sttfa:nat/commutative_plus.thm
- sttfa:nat/associative_plus.thm
- sttfa:nat/assoc_plus1.thm
- sttfa:nat/injective_plus_r.thm
- sttfa:nat/times_Sn_m.thm
- sttfa:nat/times_O_n.thm
- sttfa:nat/times_n_O.thm
- sttfa:nat/times_n_Sm.thm
- sttfa:nat/commutative_times.thm
- sttfa:nat/distributive_times_plus.thm
- sttfa:nat/distributive_times_plus_r.thm
- sttfa:nat/associative_times.thm
- sttfa:nat/times_times.thm
- sttfa:nat/times_n_1.thm
- sttfa:nat/minus_S_S.thm
- sttfa:nat/minus_O_n.thm
- sttfa:nat/minus_n_O.thm
- sttfa:nat/minus_n_n.thm
- sttfa:nat/eq_minus_S_pred.thm
- sttfa:nat/not_eq_S.thm
- sttfa:nat/not_eq_O_S.thm
- sttfa:nat/lt_to_not_zero.thm
- sttfa:nat/le_S_S.thm
- sttfa:nat/le_O_n.thm
- sttfa:nat/le_n_Sn.thm
- sttfa:nat/transitive_le.thm
- sttfa:nat/le_pred_n.thm
- sttfa:nat/monotonic_pred.thm
- sttfa:nat/le_S_S_to_le.thm
- sttfa:nat/monotonic_le_plus_r.thm
- sttfa:nat/monotonic_le_plus_l.thm
- sttfa:nat/le_plus.thm
- sttfa:nat/le_plus_n.thm
- sttfa:nat/le_plus_b.thm
- sttfa:nat/le_plus_n_r.thm
- sttfa:nat/le_plus_to_le.thm
- sttfa:nat/le_plus_to_le_r.thm
- sttfa:nat/monotonic_le_times_r.thm
- sttfa:nat/le_times.thm
- sttfa:nat/le_plus_minus_m_m.thm
- sttfa:nat/le_plus_to_minus_r.thm
- sttfa:nat/lt_to_le.thm
- sttfa:nat/transitive_lt.thm
- sttfa:nat/lt_to_le_to_lt.thm
- sttfa:nat/le_to_lt_to_lt.thm
- sttfa:nat/lt_S_to_lt.thm
- sttfa:nat/ltn_to_ltO.thm
- sttfa:nat/lt_O_S.thm
- sttfa:nat/monotonic_lt_plus_r.thm
- sttfa:nat/monotonic_lt_plus_l.thm
- sttfa:nat/monotonic_lt_times_r.thm
- sttfa:nat/monotonic_lt_times_l.thm
- sttfa:nat/lt_to_le_to_lt_times.thm
- sttfa:nat/lt_times.thm
- sttfa:nat/lt_plus_to_minus_r.thm
- sttfa:nat/lt_plus_Sn_r.thm
- sttfa:nat/not_le_Sn_O.thm
- sttfa:nat/not_le_to_not_le_S_S.thm
- sttfa:nat/not_le_S_S_to_not_le.thm
- sttfa:nat/not_le_Sn_n.thm
- sttfa:nat/lt_to_not_le.thm
- sttfa:nat/not_le_to_lt.thm
- sttfa:nat/not_lt_to_le.thm
- sttfa:nat/le_to_not_lt.thm
- sttfa:nat/decidable_le.thm
- sttfa:nat/decidable_lt.thm
- sttfa:nat/le_to_or_lt_eq.thm
- sttfa:nat/lt_O_n_elim.thm
- sttfa:nat/le_n_O_elim.thm
- sttfa:nat/lt_to_not_eq.thm
- sttfa:nat/le_n_O_to_eq.thm
- sttfa:nat/le_to_le_to_eq.thm
- sttfa:nat/plus_minus.thm
- sttfa:nat/minus_plus_m_m.thm
- sttfa:nat/plus_minus_m_m.thm
- sttfa:nat/minus_to_plus.thm
- sttfa:nat/plus_to_minus.thm
- sttfa:nat/monotonic_le_minus_l.thm
- sttfa:nat/le_plus_to_minus.thm
- sttfa:nat/monotonic_le_minus_r.thm
- sttfa:nat/minus_le.thm
- sttfa:nat/not_eq_to_le_to_lt.thm
- sttfa:nat/eq_minus_O.thm
- sttfa:nat/distributive_times_minus.thm
- sttfa:nat/minus_plus.thm
- sttfa:nat/minus_minus.thm
- sttfa:nat/minus_minus_comm.thm
- sttfa:nat/minus_le_minus_minus_comm.thm
- sttfa:nat/minus_plus_plus_l.thm
- sttfa:nat/eq_eqb.thm
- sttfa:nat/sym_eq_eqb.thm
- sttfa:nat/eq_eqb_body_O.thm
- sttfa:nat/sym_eq_eqb_body_O.thm
- sttfa:nat/eq_eqb_body_S.thm
- sttfa:nat/sym_eq_eqb_body_S.thm
- sttfa:nat/eqb_elim.thm
- sttfa:nat/eqb_n_n.thm
- sttfa:nat/eqb_true_to_eq.thm
- sttfa:nat/eqb_false_to_not_eq.thm
- sttfa:nat/eq_to_eqb_true.thm
- sttfa:nat/not_eq_to_eqb_false.thm
- sttfa:nat/eq_leb.thm
- sttfa:nat/sym_eq_leb.thm
- sttfa:nat/eq_leb_body_O.thm
- sttfa:nat/sym_eq_leb_body_O.thm
- sttfa:nat/eq_leb_body_S.thm
- sttfa:nat/sym_eq_leb_body_S.thm
- sttfa:nat/leb_elim.thm
- sttfa:nat/leb_true_to_le.thm
- sttfa:nat/le_to_leb_true.thm
- sttfa:nat/not_le_to_leb_false.thm