∀ n m, decidable (n | m)

Theorem decidable_divides : forall (n:nat.nat), forall (m:nat.nat), logic.decidable (divides n m).

theorem decidable_divides : \forall (n:nat). \forall (m:nat). (decidable) ((divides) n m).

theorem decidable_divides : forall (n:nat.nat) , forall (m:nat.nat) , ((logic.decidable) ) ((((primes.divides) ) (n)) (m)).

decidable_divides : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):logic_sttfa_th.decidable(primes_sttfa.sttfa_divides(n)(m))))

Printing for OpenTheory is not working at the moment.