Logipedia-Jumb

nat.le_to_not_lt

gcd.not_divides_to_gcd_aux

div_mod.axiom_div_aux_body_O

nat.monotonic_le_times_r

connectives.or_introl

exp.eq_exp_body_O

div_mod.let_clause_1078

nat.eq_minus_body_O

connectives.True

gcd.divides_gcd_aux_mn