apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
qed.
-interpretation "Ring mult" 'times a b =
- (cic:/matita/attic/rings/mult.con _ a b).
+interpretation "Ring mult" 'times a b = (mult _ a b).
notation "1" with precedence 89
for @{ 'one }.
-interpretation "Ring one" 'one =
- (cic:/matita/attic/rings/one.con _).
+interpretation "Ring one" 'one = (one _).
lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
intros;