proposition: Lemma test3 `{IsSemiRing R} (pa pb pc : R) : pa * (pb * pc) = pa * pb * pc.
proof: Proof. intros. apply (by_quoting (naturals_to_semiring nat R)). compute. 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