proposition: Lemma isring_scrr : is_CRing subcrr (Build_subcsetoid_crr _ _ _ Pone) submult.
proof: Proof. assert (associative submult). intros x y z; destruct x as [x xpf]; destruct y as [y ypf]; destruct z as [z zpf]; simpl; apply mult_assoc. apply (Build_is_CRing _ _ _ H). split; intro x; destruct x as [x xpf]; simpl; algebra. intros x y; destruct x as [x xpf]; destruct y as [y ypf]; simpl; apply mult_commutes. intros x y z; destruct x as [x xpf]; destruct y as [y ypf]; destruct z as [z zpf]; simpl; apply dist. simpl; apply ring_non_triv. Qed.
imports: CRings RingClass