nat.distributive_times_minus
distributive times minus
Theorem distributive_times_minus : relations.distributive (nat) times minus.
theorem distributive_times_minus : (distributive) (nat) (times) (minus) .
theorem distributive_times_minus : (((relations.distributive) (nat.nat)) ((nat.times) )) ((nat.minus) ).
distributive_times_minus : LEMMA relations_sttfa_th.distributive[nat_sttfa.sttfa_nat](nat_sttfa.times)(nat_sttfa.minus)
Printing for OpenTheory is not working at the moment.