proposition: Lemma dec_recip_swap_l x y: x / y = / (/ x * y).
proof: Proof. rewrite dec_recip_distr, involutive. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings