proposition: Lemma to_ring_respects@{} : forall a b, equiv a b -> to_ring a = to_ring b.
proof: Proof. unfold equiv;intros [pa na] [pb nb] E. unfold to_ring;simpl in *. apply (left_cancellation (+) (naturals_to_semiring N B na + naturals_to_semiring N B nb)). path_via (naturals_to_semiring N B pa + naturals_to_semiring N B nb + 0); [rewrite <-(plus_negate_r (naturals_to_semiring N B na));ring_with_nat |rewrite plus_0_r]. path_via (naturals_to_semiring N B pb + naturals_to_semiring N B na + 0); [rewrite plus_0_r| rewrite <-(plus_negate_r (naturals_to_semiring N B nb));ring_with_nat]. rewrite <-2!preserves_plus. apply ap,E. Qed.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals