proposition: Lemma Xring : @ring_theory X zero one add mul sub opp eqr.
proof: Proof. split; intros. apply monoid_iden_l. apply op_comm. apply op_assoc. apply monoid_iden_l. apply op_comm. apply op_assoc. apply ring_distributive_l. reflexivity. unfold opp. destruct (group_reverse x) as [y ?]. assumption. Qed.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid