proposition: Lemma test4 `{IsSemiRing R} (a b : R) : a * b = b * a.
proof: Proof. apply (ring_quote.Quoting.eval_eqquote R). apply (prove_prequoted (naturals_to_semiring nat R)). reflexivity. Qed.
imports: HoTT(Classes.interfaces.abstract_algebra Classes.implementations.peano_naturals Classes.orders.sum Classes.tactics.ring_tac Classes.tactics.ring_quote) HoTT.Classes.interfaces.naturals