Logipedia-Jumb

nat.decidable_le

permutation.eq_invert_permut_body_O

permutation.let_clause_1063

bool.sym_eq_match_bool_type_false

nat.minus_plus_m_m

fact.eq_fact_body_S

relations.commutative

connectives.False

nat.monotonic_lt_plus_r

nat.not_le_Sn_n