Logipedia-Jumb

gcd.gcd_aux_body

div_mod.mod

nat.not_lt_to_le

nat.le_to_not_lt

gcd.divides_gcd_aux_mn

div_mod.mod_O_n

primes.dividesb_false_to_not_divides

relations.RC_reflexive

connectives.match_Or_prop

nat.monotonic_lt_times_l