distributive times plus

Theorem distributive_times_plus : relations.distributive (nat) times plus.

theorem distributive_times_plus : (distributive) (nat) (times) (plus) .

theorem distributive_times_plus : (((relations.distributive) (nat.nat)) ((nat.times) )) ((nat.plus) ).

distributive_times_plus : LEMMA relations_sttfa_th.distributive[nat_sttfa.sttfa_nat](nat_sttfa.times)(nat_sttfa.plus)

Printing for OpenTheory is not working at the moment.