proposition: Lemma test1 `{IsSemiRing R} : forall x y : R, x + (y * x) = x * (y + 1).
proof: Proof. intros. ring_with_nat. Qed.
imports: HoTT(Classes.interfaces.abstract_algebra Classes.implementations.peano_naturals Classes.orders.sum Classes.tactics.ring_tac Classes.tactics.ring_quote)